% David Vega and Stan Warford
% Pepperdine University
% File: Vega-Paper
% !TEX TS-program = xelatex

\documentclass[12pt, fleqn, leqno]{article}

\usepackage{fontspec}
\usepackage[slantedGreek]{mathptmx}
\usepackage{amsmath, amsthm, amssymb,latexsym}
\usepackage{wasysym}                                % For temporal operators, Diamond and Box
\usepackage{eucal}                                  % For temporal operators, Until and Wait
\usepackage{booktabs}                               % For table rules
\usepackage{boxedminipage}                          % For boxing text in Hasse diagram
\usepackage{paralist}
\usepackage{ellipsis}
\usepackage{array}
%\usepackage[student]{optional}
\usepackage[doc]{optional}
%\usepackage[pub]{optional}

\newcommand{\lgap}{2pt}                             % Line gap
\newcommand{\llgap}{6pt}                            % Larger line gap
\newcommand{\lllgap}{12pt}                          % Gap between tables
\newcommand{\mymathindent}{24pt}                    % Indentation for math tabbing
\newcommand{\equivs}{\ensuremath{\;\equiv\;}}       % Equivales with space
\newcommand{\equivss}{\ensuremath{\;\;\equiv\;\;}}  % Equivales with double space
\newcommand{\nequiv}{\ensuremath{\not\equiv}}       % Inequivalent
\newcommand{\impl}{\ensuremath{\Rightarrow}}        % Implies
\newcommand{\nimpl}{\ensuremath{\not\Rightarrow}}   % Does not imply
\newcommand{\foll}{\ensuremath{\Leftarrow}}         % Follows from
\newcommand{\nfoll}{\ensuremath{\not\Leftarrow}}    % Does not follow from

\defaultfontfeatures{Mapping=tex-text}
\setmainfont[Ligatures={Common}]{Times}
\setsansfont{Helvetica}
\setmonofont[Scale=.95]{Courier}

% Macros for Temporal Operators
\newcommand{\Until}{\;\mathcal{U}\;}
\newcommand{\Wait}{\;\mathcal{W}\;}
\newcommand{\Next}{\;\,\text{\raisebox{3.5pt}{\circle{6}}}}
\newcommand{\Event}{\Diamond\,}
\newcommand{\Always}{\Box\,}

\DeclareMathOperator{\divides}{divides}

\newcommand{\myqed}{\rule[-.23ex]{1.2ex}{2.0ex}}
\newcommand{\myqedtab}{\hspace{384pt}}              % For flush right qed symbol in tabbing environment. No longer used.
\newcommand{\spacer}{\vspace{-30pt}}
\newcommand{\firstspacer}{\vspace{-26pt}}

% Thanks to David Gries for sharing the following macros
% Macros for quantifications.
\newcommand{\thedr}{\rule[-.25ex]{.32mm}{1.75ex}}   % Symbol that separates dummy from range in quantification
\newcommand{\dr}{\;\,\thedr\,\;}                    % Symbol that separates dummy from range, with spacing
\newcommand{\rb}{:}                                 % Symbol that separates range from body in quantification
\newcommand{\drrb}{\;\thedr\,{:}\;}                 % Symbol that separates dummy from body when range is missing
\newcommand{\all}{\forall}                          % Universal quantification
\newcommand{\ext}{\exists}                          % Existential quantification

% Macros for proof hints
\newcommand{\Gll} {\langle}                         % Open hint
\newcommand{\Ggg} {\rangle}                         % Close hint
\newlength{\Glllength}                              % Length of open hint symbol
\settowidth{\Glllength}{$.\Gll$}
\newcommand{\Hint}[1]     {\ \ \ $\Gll              \mbox{#1} \Ggg$ }   % Single line hint
\newcommand{\Hintfirst}[1]{\ \ \ $\Gll              \mbox{#1}$ }        % First line of multiline hint
\newcommand{\Hintmid}[1]  {\ \ $\hspace{\Glllength} \mbox{#1}$ }        % Middle line of multiline hint
\newcommand{\Hintlast}[1] {\ \ $\hspace{\Glllength} \mbox{#1} \Ggg$ }   % Last line of multiline hint

% Single and double quotes
\newcommand{\Lq}{\mbox{`}}
\newcommand{\Rq}{\mbox{'}}
\newcommand{\Lqq}{\mbox{``}}
\newcommand{\Rqq}{\mbox{''}}

\oddsidemargin  0.0in
\evensidemargin 0.0in
\textwidth      6.0in
\headheight     0.0in
\topmargin      0.0in
\textheight=8.5in
%\parindent=0in
%\pagestyle{plain}

\pagestyle{myheadings} 
\markboth{\textbf{Draft} (\today)} {\textbf{Draft} (\today)}

\opt{student}{
\title{An Equational Deductive System\\for Linear Temporal Logic (Student)}
}

\opt{doc}{
\title{An Equational Deductive System\\for Linear Temporal Logic (Complete)}
}

\opt{pub}{
\title{An Equational Deductive System\\for Linear Temporal Logic}
}

\author{David Vega\thanks{Research supported by Tooma Undergraduate Research Fellowship Program, Summer 2009
        and academic year 2009-10.}\\
   J. Stanley Warford\\
   Computer Science Department\\
   Pepperdine University\\
   Malibu, CA 90263}
\date{} % Required for no date to appear in heading

\begin{document}
\maketitle
\begin{abstract}
This paper presents an equational deductive system for linear temporal logic.
It differs from previous developments of temporal logic in several respects.
First, the proofs are given in the equational logic developed by Dijkstra and Scholten, and extended by Gries and Schneider, as opposed to the older Hilbert-style logics.
Second, it includes all known linear temporal logic theorems plus many new and interesting theorems.
Third, although space limitations preclude giving a proof of every theorem in this paper,
every theorem has been proved with equational logic.
The summary of equational logic is minimal, and the paper can serve as an introduction to linear temporal logic.
\end{abstract}

\thispagestyle{plain}

\section{Introduction}

All axiomatic logic systems have three components --- inference rules, axioms, and theorems.
Both inference rules and axioms are assumed.
Theorems are proved from axioms using inference rules.
From a computational systems perspective, the inference rules process axioms as input and produce theorems as output.
Figure \ref{logic-systems} shows the parallel between traditional computational systems and axiomatic logic systems.
In the same way that a processor executes program statements with input to produce output, a proof uses inference rules with axioms to produce theorems.

In a conventional computational system, placement of the hardware/software boundary is a design decision.
Any given computational task can be implemented either in hardware or in software.
The tradeoff in such systems is usually between speed of execution and flexibility.
Usually, a task implemented in hardware executes faster than if it is implemented in software.
However, once implemented in hardware a task is more difficult to modify or extend than if it is implemented in software.
One goal of RISC design is to simplify the hardware by moving tasks from hardware to software.
For example, CISC machines provide complex addressing modes with hardware circuits to compute array cell addresses.
The equivalent address computation is done in software in a RISC machine.

A similar design decision exists in axiomatic logic systems with the placement of the inference rule/axiom boundary.
It is possible to have two different logic systems produce equivalent sets of theorems but with different sets of inference rules and axioms.
What is an inference rule in one system might be a corresponding axiom in the other.
The tradeoff is more subjective in logic systems, as there is apparently no metric of goodness that can be quantified as objectively as can the speed of execution in computational systems.

This paper presents a logic system that places the boundary between inference rules and axioms to minimize the number of inference rules.
We maintain that the primary advantage of such a system is a human one.
That is, proofs in such systems are easier to understand and to design than in other systems.

\begin{figure}[t]
\centering
\begin{picture}(440,46)
\thicklines
\put(0,24) {\fbox{\parbox{36pt}{\centering Input}}}
\put(43,28) {\vector(1,0){20}}
\put(63,24) {\fbox{\parbox{56pt}{\centering Processing}}}
\put(126,28) {\vector(1,0){20}}
\put(146,24) {\fbox{\parbox{42pt}{\centering Output}}}
\put(40,0) {Computational systems}

\put(220,24) {\fbox{\parbox{36pt}{\centering Axioms}}}
\put(263,28) {\vector(1,0){20}}
\put(283,24) {\fbox{\parbox{56pt}{\centering Inference\\rules}}}
\put(346,28) {\vector(1,0){20}}
\put(366,24) {\fbox{\parbox{48pt}{\centering Theorems}}}
\put(250,0) {Axiomatic logic systems}

\end{picture}
\caption{Computational systems and axiomatic logic systems.
\label{logic-systems}}
\end{figure}

\subsubsection*{Propositional logic systems}

Propositional calculus is a formal system of logic based on the unary operator negation $\neg$,
the binary operators conjunction $\land$, disjunction $\lor$, implies $\impl$ (also written $\rightarrow$),
and equivalence $\equiv$ (also written $\leftrightarrow$),
variables (lowercase letters $p$, $q$, \dots), and the constants $true$ and $false$.
Hilbert-style logic systems, $\mathcal{H}$, are the deductive logic systems traditionally used in mathematics to describe the propositional calculus.
Typical of such descriptions with applications to computer science is the text by Ben-Ari \cite{Ben}.
A key feature of such systems is their multiplicity of inference rules and the importance of modus ponens as one of them.

In the late 1980's, Dijkstra and Scholten \cite{DandS}, and Feijen \cite{Feij} developed a method of proving program correctness with a new logic based on an equational style.
This equational deductive system, $\mathcal{E}$, is the basis of books by Kaldewaij \cite{Kald} and Cohen \cite{Cohen}.
In contrast to $\mathcal{H}$ systems, $\mathcal{E}$ has only four inference rules --- Substitution, Leibniz, Equanimity, and Transitivity.
In $\mathcal{E}$, modus ponens plays a secondary role.
It is not an inference rule, nor is it assumed as an axiom, but instead is proved as a theorem from the axioms using the inference rules.

Gries and Schneider \cite{Gries1995, Gries1995145} show that $\mathcal{E}$, also known as a \textit{calculational} system, has several advantages over traditional logic systems.
The primary advantage of $\mathcal{E}$ over $\mathcal{H}$ systems is that the equational system has only four proof rules, with inference rule Leibniz as the primary one.
Roughly speaking, Leibniz is ``substituting equals for equals,'' hence the moniker \textit{equational} deductive system.
In contrast, $\mathcal{H}$ systems rely on a more extensive set of inference rules.
We find proofs in $\mathcal{E}$ easy to understand and to teach, because the substitution of equals for equals is so common in elementary algebraic manipulations.

Another major advantage of $\mathcal{E}$ over $\mathcal{H}$ systems is the sequential format of its proof syntax.
Proofs in $\mathcal{H}$ systems have a bottom-up tree structure, which is sequentialized with multiple references to previously numbered lines.
For example, a proof of formula $f_2$ might begin by establishing the validity  of a formula $f_1$ on lines 1 through 4.
Then, on lines 5 through 9, it might establish the validity of $f_1\impl f_2$.
Then, on line 10, it would refer back to lines 4 and 9 and invoke modus ponens to establish the validity of $f_2$.

In contrast, proofs in $\mathcal{E}$ have a top-down structure and proceed sequentially with each step self-contained.
There is no need to number the lines in a proof in $\mathcal{E}$ because reference is never made to a previous intermediate step of the proof.
Instead, each line depends only on the immediately preceding line by invoking a previously-proved theorem or an axiom.

There is an analogy between the proof style of $\mathcal{H}$ systems versus the proof style of $\mathcal{E}$ and the unstructured goto style of programming versus structured programming.
In the same way that the goto statement produces spaghetti code that is more difficult to understand than structured code, proofs in $\mathcal{H}$ systems are more difficult to understand than proofs in $\mathcal{E}$.
It is perhaps not coincidental that Dijkstra, who ignited the goto controversy with his famous CACM letter \cite{Dijkstra:1968:LEG:362929.362947}, was the prime developer of $\mathcal{E}$.

We agree with Gries and Schneider \cite{LADM} that, ``We need a style of logic that can be used as a tool in every-day work.
In our experience, an equational logic, which is based on equality and Leibniz's rule for substitution of equals for equals, is best suited for this purpose.''
These advantages of $\mathcal{E}$ over $\mathcal{H}$ systems are primarily \textit{human} advantages, not necessarily machine advantages.
That is, the motivation behind this work is based on teaching and human understanding, as opposed to machine theorem provers or proof assistants.

In 1994, Gries and Schneider published \textit{A Logical Approach to Discrete Math} (LADM) \cite{LADM}, in which they first develop $\mathcal{E}$ for propositional and predicate calculus, and then extend it to a theory of sets, a theory of sequences, relations and functions, a theory of integers, recurrence relations, modern algebra, and a theory of graphs.
Using equational logic as a tool, LADM brings all the advantages of $\mathcal{E}$ to these additional knowledge domains.
The treatment is in marked contrast to the traditional one exemplified by the classic text by Rosen \cite{Rosen}.

\subsubsection*{Linear temporal logic systems}

Linear temporal logic describes how the truth values of propositions change over time.
It extends the propositional operators with the unary operators \textit{next} $\Next$, \textit{eventually} $\Event$, and \textit{always} $\Always$, and the binary operators \textit{until} $\Until$ and \textit{wait} $\Wait$.
All treatments of linear temporal logic use $\mathcal{H}$ systems instead of $\mathcal{E}$.
Typical are Ben-Ari \cite{Ben2}, Emerson \cite{Emer}, Kröger and Merz \cite{Kroger}, Manna and Pnueli \cite{Manna}, and Schneider \cite{Schn}.

Each of these authors describes the semantics of the above temporal operators and provides an axiomatization for linear temporal logic.
One characteristic of these $\mathcal{H}$ systems is the introduction of temporal inference rules along with temporal axioms from which temporal theorems are proved.
Section \ref{comparison-previous-work} summarizes these systems and compares them with this work.

Our institution has used LADM at the introductory undergraduate level since its publication, and the equational proof style has consequently permeated the computer science curriculum.
A problem arises, however, when those who are schooled in $\mathcal{E}$ study concurrency and need the correctness proof tools of linear temporal logic, because $\mathcal{E}$ has not yet been extended to this knowledge domain.
Schneider \cite{Schn} appears to be the only treatment of linear temporal logic that includes a discussion of $\mathcal{E}$.
Although he presents a temporal logic equational proof justification, the only appearance of an equational proof of a temporal logic theorem is a single example on page 74.

To solve the above problem, this paper presents a comprehensive equational deductive system suitable for introducing those versed in $\mathcal{E}$ to linear temporal logic.
In the same way that LADM brings the advantages of $\mathcal{E}$ to set theory and other mathematical domains, this paper brings the advantages of $\mathcal{E}$ to linear temporal logic.

This axiomatization follows the spirit of $\mathcal{E}$ in its design to minimize the number of inference rules.
A unique characteristic of this system is the complete absence of any temporal inference rules.
It extends the propositional calculus of LADM using only the same four inference rules of $\mathcal{E}$ along with additional temporal axioms.
In our judgment, the absence of temporal inference rules brings the same clarity to linear temporal logic that $\mathcal{E}$ brings to the propositional calculus.

The paper also adds to the linear temporal logic literature by proving many interesting and previously unknown theorems.
It is comprehensive, as we have tried to include all known linear temporal theorems described in the literature.
Although space limitations preclude giving a proof of every theorem in this paper, we have proved every theorem with $\mathcal{E}$.

Section 2 describes the deductive axioms and the proof rules for $\mathcal{E}$.
It also defines the syntax and semantics of linear temporal logic.
Section 3 presents the equational deductive system for linear temporal logic.
Section 4 summarizes previous linear temporal logic axiomatization systems and compares them with the current work.

\section{Background}

The first section below summarizes the equational system $\mathcal{E}$ from LADM.
The summary is minimal, and assumes the reader is familiar with the propositional and predicate calculus.
The second section introduces temporal logic and assumes no prior familiarity with it.
The paper can serve as an introduction to linear temporal logic.

\subsection{Equational Deductive Systems}\label{sec-equational-deductive-systems}

\subsubsection*{Propositional calculus}

Expressions are the basis of propositional calculus in the equational system.
Propositional theorems are simply boolean expressions that are true in all states.
The definition of an expression has four parts:
\begin{itemize}[$\bullet$]
\item A constant or variable is an expression.
\item If $E$ is an expression, then $(E)$ is an expression.
\item If $\triangleright$ is a unary prefix operator and $E$ is an expression, then $\triangleright E$ is an expression with operand $E$.
\item If $\star$ is a binary infix operator and $D$ and $E$ are expressions, then $D \star E$ is an expression with operands $D$
and $E$.
\end{itemize}
By convention, upper-case letters ({\itshape e.g.\/} $X$, $Y$, \dots) represent expressions,
and lower-case letters ({\itshape e.g.\/} $x$, $y$, \dots) represent variables.
In the propositional calculus, the constants are {\itshape true\/} and {\itshape false\/}.

Figure \ref{precedence-table} is the table of precedences.
Textual substitution has the highest precedence.
All the unary operators have the next highest precedence.
They are necessarily right associative.
For example, $\neg \Next \neg p$ means $\neg (\Next (\neg p))$.
In this system, two binary operators that have the same precedence require parentheses to disambiguate.
As in LADM, conjunction $\land$ and disjunction $\lor$ have the same precedence so that $p\land q\lor r$
must be disambiguated as either $(p\land q)\lor r$ or $p\land (q\lor r)$.
This contrasts with many systems in which conjunction has higher precedence than disjunction.

\begin{figure}[t]
\centering
\setlength\extrarowheight{2pt}
\begin{tabular}{lr}
\hline
$[x := e]$ (textual substitution) & Highest precedence\\
$\neg$\quad $\Next$\quad $\Event$\quad $\Always$ &\\
$\Until$\quad $\Wait$ &\\
$=$\quad (conjunctional) &\\
$\lor$\quad $\land$ &\\
$\impl$\quad $\foll$ &\\
$\equiv$ \quad (associative) & Lowest precedence\\
\hline
\end{tabular}
\caption{Precedence of the propositional and temporal logic operators.
\label{precedence-table}}
\end{figure}

Also consistent with the equational system of LADM but different from most other deductive logic systems
is the difference between operators equals $=$ and equivales $\equiv$.
Equals applies to any mathematical type including, {\itshape e.g.\/}, boolean, natural number, and set.
Equivales applies only to boolean, and is commonly denoted $\leftrightarrow$ in other systems.
Another difference is that equals is conjunctive, while equivales is associative.
For example, the expression $p = q = r$ has conjunctive meaning $(p = q) \land (q = r)$, while the expression $p \equiv q \equiv r$
can be taken as either $(p \equiv q) \equiv r$ or $p \equiv (q \equiv r)$.
This property of equivales is the first axiom in the equational deductive system of LADM.

\subsubsection*{Inference rules}

The inference rules for the equational deductive system are Substitution, Leibniz, Equanimity, and Transitivity.
\[
\textbf{Substitution:}\quad \frac{E}{E[z:=F]}
\]
\[
\textbf{Leibniz:}\quad \frac{X=Y}{E[z:=X]=E[z:=Y]}
\]
\[
\textbf{Equanimity:}\quad \frac{X, \quad X=Y}{Y}
\]
\[
\textbf{Transitivity:}\quad \frac{X=Y, \quad Y=Z}{X=Z}
\]
where the square bracket in $E[z:=F]$ indicates textual substitution of expression $F$ for variable $z$
everywhere $z$ occurs in expression $E$.
In a typical proof, Substitution and Leibniz are explicit, while Equanimity and Transitivity are implicit.

Substitution allows the generalization of a single theorem to represent an infinite number of theorems.
For example, because $p\impl false \equiv \lnot p$ is a theorem, then, with $p:=p\land q$, the expression
$(p\land q)\impl false \equiv \lnot (p\land q)$ is also a theorem.

Roughly speaking, Leibniz allows for the substitution of equals for equals in a proof step.
The general form of a proof step is
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \=  \kill
  \> \>   $E[z:=X]$\\[\lgap]
  \> $=$  \>  \Hint{$X=Y$} \\[\lgap]
  \> \>   $E[z:=Y]$
\end{tabbing}
where the expression enclosed in angle brackets $\Gll\;\Ggg$, called the ``hint'', is the justification for the step.

An example of a proof step from the proof of theorem (\ref{E:eventAlwaysPAndAlwaysEventQ}) in Section \ref{section-always-continued} is
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \>   $\Always (\Always p \land \Event q) \impl \Always\Event (p \land q)$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
\> \>   $\Always \Always p \land \Always\Event q \impl \Always\Event (p \land q)$
\end{tabbing}
This proof step uses the previously proved theorem (\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$,
which is $\Always (p \land q) \equiv \Always p \land \Always q$.
The justification in the hint $X=Y$ comes from inference rule Substitution, with the textual substitution of $\Always p$ for $p$ and $\Event q$ for $q$ in (\ref{E:distAlwaysAnd}) as follows
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\Always (p \land q) \equiv \Always p \land \Always q)[p,q:=\Always p, \Event q]:\quad \Always (\Always p \land \Event q) \equiv \Always \Always p \land \Always \Event q$
\end{tabbing}
The expressions in Leibniz for the step are
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $E:\quad z \impl \Always\Event (p \land q)$\\[\lgap]
  \> $X:\quad \Always (\Always p \land \Event q)$\\[\lgap]
  \> $Y:\quad \Always \Always p \land \Always \Event q$
\end{tabbing}
The textual substitutions are
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $E[z:=X]:\quad \Always (\Always p \land \Event q) \impl \Always\Event (p \land q)$\\[\lgap]
  \> $E[z:=Y]:\quad \Always \Always p \land \Always\Event q \impl \Always\Event (p \land q)$
\end{tabbing}

The proof of a theorem consists of showing the equivalence of that theorem to a previously proved theorem
through a sequence of the proof steps.
For example, here is a one-step proof of (\ref{E:linearity}) $\Next p \equiv \neg\Next\neg p$ in Section \ref{section-next}.

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \kill
  \> \>   $\Next p \equiv \neg\Next\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(3.11) $\neg p \equiv q \equiv p \equiv \neg q$ with $p,q := \Next\neg p, \Next p$} \\[\lgap]
  \> \>   $\neg\Next p \equiv \Next\neg p$ \\[\lgap]
  \> which is (\ref{E:selfDual}), Self-dual. \quad \myqed
\end{tabbing}
In a proof hint, numeric references that contain a decimal point, such as (3.11) above, refer to a theorem in $\mathcal{E}$ from LADM.
Equanimity is implicit in the proof.
Because $\neg\Next p \equiv \Next\neg p$ (\textit{i.e.} $X$) is a previous theorem, and $\neg\Next p \equiv \Next\neg p$ is equivalent to $\Next p \equiv \neg\Next\neg p$ (\textit{i.e.} $X=Y$), by equinimity $\Next p \equiv \neg\Next\neg p$ (\textit{i.e.} $Y$) is proved.

Transitivity of equality allows a derivation to be given as a sequence of equivalent expressions, which, at the end,
proves the equivalence of the first expression in the sequence with the last expression in the sequence.
For example, here is a two-step proof of (\ref{E:idemUntil}) Idempotency of $\Until$, $p \Until p \equiv p$ in Section \ref{section-until}.

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until p\equiv p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $p \lor (p \land \Next(p \Until p))\equiv p$\\[\lgap]
  \> $=$  \>  \Hint{(3.43b) Absorption, $p \lor (p \land q) \equiv p$ with $q := \Next (p \Until p)$}\\[\lgap]
  \> \>   $p\equiv p$\\[\lgap]
  \> which is (3.5) Reflexivity of $\equiv$. \quad \myqed
\end{tabbing}
Transitivity of equality is implicit in the proof.
Because $p \Until p\equiv p$ is equivalent to $p \lor (p \land \Next(p \Until p))\equiv p$ (\textit{i.e.} $X=Y$),
and $p \lor (p \land \Next(p \Until p))\equiv p$ is equivalent to $p\equiv p$ (\textit{i.e.} $Y=Z$),
by transitivity $p \Until p\equiv p$ is equivalent to $p\equiv p$ (\textit{i.e.} $X=Z$).

\subsubsection*{Proof technique metatheorems}

The logic system $\mathcal{E}$ of \cite{LADM} has 13 axioms for the propositional calculus from which theorems are deduced
with the above inference rules in the equational style.
The system also contains a number of metatheorems based on properties of equivalence and implication, which allow the
proof style to be extended.
Here are four of the proof technique metatheorems.
\begin{tabbing}
(9.9.9)\;\=(m)\;\=\kill
(4.4)\>\textbf{Deduction (assume conjuncts of antecedent):}\\[\lgap]
      \>To prove $P_{1}\land P_{2}\impl Q$, assume $P_{1}$ and $P_{2}$, and prove $Q$.\\[\lgap]
      \>You cannot use textual substitution in $P_{1}$ or $P_{2}$.\\[\lgap]
(4.7)\>\textbf{Mutual implication:}\quad To prove $P\equiv Q$, prove $P\impl Q$ and $Q\impl P$.\\[\lgap]
(4.7.1)\>\textbf{Truth implication:}\quad To prove $P$, prove $true\impl P$.\\[\lgap]
(4.12)\>\textbf{Contrapositive:}\quad To prove $P\impl Q$, prove $\neg Q\impl \neg P$.
\end{tabbing}

The validity of each metatheorem is established from the theorems of the propositional calculus and the inference rules.
Deduction is established by showing that any deductive proof has an equivalent equational proof.
Mutual implication is based on (3.80), Truth implication is based on (3.73), and Contrapositive is based on (3.61).
\begin{tabbing}
(9.99)\;\=(m)\;\=\kill
(3.80)\>\textbf{Mutual implication:}\quad $(p\impl q) \land (q\impl p) \equivs (p\equiv q)$\\[\lgap]
(3.73)\>\textbf{Left identity of $\impl$ :}\quad $true\impl p \equivs p$\\[\lgap]
(3.61)\>\textbf{Contrapositive:}\quad $p\impl q \equivs \neg q\impl \neg p$
\end{tabbing}

The proof format is extended to the case where the theorem to be proved is of the form $P \equiv Q$.
For theorems of this form, the proof may begin with the left hand side and show equivalence to the right hand side through a sequence of proof steps.
This proof style is established by showing that such a proof is equivalent to an equational proof and is based on (3.5).
\begin{tabbing}
(9.9)\;\=(m)\;\=\kill
(3.5)\>\textbf{Reflexivity of $\equiv$ :}\quad $p\equiv p$
\end{tabbing}
For example, the following proof is the preferred style for the previous proof of (\ref{E:idemUntil}).

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \kill
  \> \>   $p \Until p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $p \lor (p \land \Next(p \Until p))$\\[\lgap]
  \> $=$  \>  \Hint{(3.43b) Absorption, $p \lor (p \land q) \equiv p$ with $q := \Next (p \Until p)$}\\[\lgap]
  \> \>   $p$ \quad \myqed
\end{tabbing}

Gries and Schneider also extend the proof format to incorporate implication using its transitive properties
with itself and with equivales.
Instead of proving a theorem of the form $P\impl Q$ to be equivalent to a previously proved theorem,
$P$ can be shown to imply $Q$, or $Q$ can be shown to follow from $P$.
The following mutual transitivity theorems justify this extension.
\begin{tabbing}
(9.99)\;\=(m)\;\=\kill
(3.82)\>\textbf{Transitivity:}\\
      \> (a)\> $(p\impl q) \land (q\impl r) \impl (p\impl r)$\\[\lgap]
      \> (b)\> $(p\equiv q) \land (q\impl r) \impl (p\impl r)$\\[\lgap]
      \> (c)\> $(p\impl q) \land (q\equiv r) \impl (p\impl r)$
\end{tabbing}
An example is a proof of (\ref{E:impEvent}) $p \impl \Event p$ in Section \ref{section-event}.

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionEvent}) Expansion of $\Event$}\\[\lgap]
  \> \>   $p \lor \Next\Event p$\\[\lgap]
  \> $\foll$  \>  \Hint{(3.76a) Weakening $p\impl p\lor q$ with $q:=\Next\Event p$}\\[\lgap]
  \> \>   $p$ \quad \myqed
\end{tabbing}
Because $\Event p$ equivales $p \lor \Next\Event p$, and $p \lor \Next\Event p$ follows from $p$, it follows by
mutual transitivity that $\Event p$ follows from $p$.

The following two theorems from LADM provide a further extension to proof steps with implication.
\begin{tabbing}
(9.99)\;\=(m)\;\=\kill
(4.2)\>\textbf{Monotonicity of $\lor$ :}\quad $(p\impl q) \impl (p\lor r \impl q\lor r)$\\[\lgap]
(4.3)\>\textbf{Monotonicity of $\land$ :}\quad $(p\impl q) \impl (p\land r \impl q\land r)$
\end{tabbing}
They are required to justify an implication when the antecedent of the implication is a conjunct or disjunct.
For example, here is a proof step where the antecedent $p\Until q$ is a disjunct in the expression $\Always p\lor p \Until q$.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Always p\lor p \Until q$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:eventuality}) Eventuality and (4.2) Monotonicity of $\lor$} \\[\lgap]
\> \> $\Always p\lor \Event q$
\end{tabbing}
Previously proved theorem (\ref{E:eventuality}) Eventuality is $p \Until q \impl \Event q$.
The application of (4.2) is with the following textual substitution.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $((p\impl q) \impl (p\lor r \impl q\lor r))[p,q,r := p\Until q, \Event q, \Always p]$\\[\lgap]
\> $=$ \> \Hint{Textual substitution} \\[\lgap]
\> \> $(p\Until q\impl \Event q) \impl (p\Until q\lor \Always p \impl \Event q\lor \Always p)$
\end{tabbing}
In other words, because $p\Until q$ implies $\Event q$, $p\Until q\lor \Always p$ implies $\Event q\lor \Always p$.

\subsubsection*{Predicate calculus}

The predicate calculus of the equational system has a consistent quantification notation that applies to Abelian monoids in both mathematics and logic.
Denoting a general Abelian monoid as the infix operator $\star$, the form of a quantification is
\[
(\star\; dummies\dr range\rb body)
\]
All quantifications have explicit scope for the dummy variable denoted by the outer parentheses.
Within the parentheses the quantification consists of three parts:
\begin{itemize}
\item the infix operator $\star$ and dummy variable(s),
\item the range, which is a boolean expression, and
\item the body, which is an expression that is type compatible with the operator $\star$.
\end{itemize}
A vertical bar separates the operator and dummy variable from the range, and a colon separates the range from the body.
An abbreviation is to omit the range when it is $true$.
For example, $(\all i\drrb P)$ is an abbreviation for $(\all i\dr true \rb P)$.

For example, the standard mathematical notation for writing the sum of the squares of the first $n$ positive integers is
\[
\sum_{i=1}^{n}i^2
\]
where $\star$ is Abelian monoid $+$, and $\upSigma$ is the quantified symbol for addition.
The equational notation for the same expression is
\[
(\upSigma i\dr 1\le i\le n \rb i^2)
\]
Similarly, the standard logic notation for writing that there exists a number between 10 and 20 inclusive that divides $n$ is
\[
\ext i(10\le i\le 20 \land \divides(i,n))
\]
where $\star$ is Abelian monoid $\lor$, $\ext$ is the quantified symbol for disjunction, and $\divides$ is a predicate that is true when $i$ divides $n$.
The equational notation for the same expression is
\[
(\ext i\dr 10\le i\le 20 \rb \divides(i,n))
\]

Predicate calculus in the equational system of LADM begins with nine general axioms that apply to all Abelian monoids.
For example, here are the first two axioms.
\begin{tabbing}
(99.99)\;\=(m)\;\=\kill
For symmetric and associative binary operator $\star$ with identity $u$.\\[\lgap]
(8.13)\>\textbf{Axiom, Empty range:}\quad $(\star x \dr false \rb P) =u$\\[\lgap]
(8.14)\>\textbf{Axiom, One-point rule:}\quad Provided $\neg occurs(\Lq x\Rq ,\Lq E\Rq)$,\\[\lgap]
      \>$(\star x\dr x=E\rb P) = P[x:=E]$
\end{tabbing}
It has two axioms for universal quantification.
\begin{tabbing}
(99.99)\;\=(m)\;\=\kill
(9.2)\>\textbf{Axiom, Trading:}\quad $(\all x\dr R\rb P)\equiv (\all x\drrb R\impl P)$\\[\lgap]
(9.5)\>\textbf{Axiom, Distributivity of $\lor$ over $\all$ :}\quad Provided $\neg occurs(\Lq x\Rq ,\Lq P\Rq)$,\\[\lgap]
      \>$P\lor (\all x\dr R\rb Q)\equiv (\all x\dr R\rb P\lor Q)$
\end{tabbing}
And it has one axiom for existential quantification.
\begin{tabbing}
(99.99)\;\=(m)\;\=\kill
(9.17)\>\textbf{Axiom, Generalized De Morgan:}\quad $(\ext x\dr R\rb P)\equiv \neg (\all x\dr R\rb \neg P)$
\end{tabbing}

\subsection{Linear Temporal Logic}

The operators of propositional calculus, $\neg$, $=$, $\land$, $\lor$, $\impl$, $\foll$, and $\equiv$ are static.
That is, they apply at a single point in time.
Each operator has a truth table that dictates how to evaluate the truth value of an expression.
A state is an assignment of a truth value to each variable in the expression.
A given boolean expression may be false in all states, true in some states and false in others, or true in all states, in which case the expression is known as a theorem or validity or tautology.

The operators of temporal logic, $\Next$, $\Event$, $\Always$, $\Until$, and $\Wait$ are dynamic.
That is, they do not apply at a single point in time, but apply over an infinite sequence of states.
Each state corresponds to a discrete point in time that represents one point in the execution of a program,
possibly having several threads running concurrently but whose instruction executions have been serialized.
As one instruction in the program executes, the state changes, and hence the truth value of an expression may change as well.

A model $\sigma$ is an infinite sequence of the form
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $\sigma: s_0, s_1, s_2, \dots$
\end{tabbing}
where $s_0$ is the initial state and each state $s_i, 0 \le i$ is the state at time $i$.

For example, suppose $x$ is an integer variable whose value varies at each step of the computation.
Then, $x$ and the expression $x\ge 10$, known as a state expression, might evolve as follows.\\[\lllgap]
\begin{tabular}{c|ccccccc}
  $\sigma$      & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & \dots \\
  \hline
  $x$           & 8     & 9     & 10    & 11    & 12    & \dots\\
  $x\ge 10$     & F     & F     & T     & T     & T     & \dots
\end{tabular}\\[\lllgap]
The bottom row shows the evaluation of the state expression for each state in the sequence.
Temporal logic extends propositional logic by considering the evolution of expression evaluations in time.
For example, if you assume that $x$ in the above sequence keeps increasing by one you can assert
informally in English, ``For the sequence $\sigma$, eventually $x\ge 10$ will always be true.''

The notation
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\sigma, j) \models p$
\end{tabbing}
means that the expression $p$ holds at position $j$ in a sequence $\sigma$.
In the above example,
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\sigma, 3) \models x\ge 10$.
\end{tabbing}
The symbol $\models$ means ``satisfies'', so the above expression is read as
``State 3 of sequence $\sigma$ satisfies $x\ge 10$.''
Or, using ``holds'', the same expression is read as, ``$x\ge 10$ holds in state 3 of sequence $\sigma$.''
The following sections use $\models$ to formalize the interpretation of each temporal operator.

There is a distinction between the constant $true$ and the truth value of an expression T in a given state.
The constant $true$ is an expression that evaluates to T in every state.
Similarly, there is a distinction between the constant $false$ and the truth value of an expression F in a given state.
The constant $false$ is an expression that evaluates to F in every state.\\[\lllgap]
\begin{tabular}{c|ccccccc}
  $\sigma$      & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & \dots \\
  \hline
  $true$        & T     & T     & T     & T     & T     & \dots\\
  $false$       & F     & F     & F     & F     & F     & \dots
\end{tabular}

\subsubsection*{The \textit{next} operator $\Next$}

The semantics of the unary prefix operator $\Next$ are
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\sigma, j) \models \Next p$ \quad iff \quad $(\sigma, j+1) \models p$
\end{tabbing}
That is, $\Next p$ holds at position $j$ iff $p$ holds at position $j+1$.

For example, in the following sequence $\Next 10\le x< 13$ holds at state $s_1$ because $10\le x< 13$ holds at state $s_2$.\\[\lllgap]
\begin{tabular}{c|ccccccccc}
  $\sigma$             & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & $s_5$ & $s_6$ & \dots \\
  \hline
  $x$                  & 8     & 9     & 10    & 11    & 12    & 13    & 14    & \dots\\
  $10\le x< 13$        & F     & F     & T     & T     & T     & F     & F     & \dots\\
  $\Next 10\le x< 13$  & F     & T     & T     & T     & F     & F     & F     & \dots
\end{tabular}\\[\lllgap]
In other words,
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\sigma, 1) \models \Next 10\le x< 13$ \quad because \quad $(\sigma, 2) \models 10\le x< 13$
\end{tabbing}
Furthermore, $\Next 10\le x< 13$ does not hold at state $s_4$ even though $10\le x< 13$ does hold in that state, because $10\le x< 13$ does not hold in state $s_5$.

\subsubsection*{The \textit{until} operator $\Until$}

The semantics of the binary infix operator $\Until$ are
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\sigma, j) \models p \Until q$ \quad iff \quad $(\ext k \dr k \ge j \rb (\sigma,k) \models q \land
      (\all i \dr j\le i < k \rb (\sigma,i) \models p))$
\end{tabbing}
If $p \Until q$ holds at state $s_j$, then $p$ holds at state $s_j$ and continues to hold at every state
after $s_j$ until $q$ holds at some future state.
$p \Until q$ guarantees that $q$ will eventually hold at some future state, and that $p$ will continue to hold until then.
After the state in which $q$ holds for the first time, there are no restrictions on either $p$ or $q$.

For example, suppose $x$ and $y$ evolve in the computation as follows.\\[\lllgap]
\begin{tabular}{c|ccccccccccc}
  $\sigma$                  & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & $s_5$ & $s_6$ & $s_7$ & $s_8$ & $s_9$ & \dots \\
  \hline
  $x$                       & $-1$  & 0     & 1     & 2     & 3     & 4     & 5     &  6    &  7    &  8    &  \dots\\
  $y$                       & 9     & 8     & 7     & 6     & 5     & 4     & 3     &  2    &  1    &  0    &  \dots\\
  $0<x<y$                   & F     & F     & T     & T     & T     & F     & F     &  F    &  F    &  F    &  \dots\\
  $2\le y<5$                & F     & F     & F     & F     & F     & T     & T     &  T    &  F    &  F    &  \dots\\
  $(0<x<y)\Until(2\le y<5)$ & F     & F     & T     & T     & T     & T     & T     &  T    &  F    &  F    &  \dots
\end{tabular}\\[\lllgap]
The bottom row shows the evaluation of the expression $p\Until q$ where $p\equiv 0<x<y$ and $q\equiv 2\le y<5$.
In states $s_0$ and $s_1$, $p\Until q$ is false because both $p$ and $q$ are false.
Starting at state $s_2$, $p\Until q$ is true because in that state $p$ is true and will remain true until $q$
eventually becomes true in state $s_5$.

From the semantics of $p\Until q$, if $q$ is true in any state, then $p\Until q$ is true in that state regardless of $p$.
For example, not only is $p\Until q$ true in state $s_5$, before which $p$ was true in several preceding states,
it is also true in states $s_6$ and $s_7$, because in those states $q$ is true.
This behavior of $p\Until q$ comes from the empty range and one-point rules \cite{LADM} of the predicate calculus in the case that
$q$ holds in state $s_j$ and $k=j$.

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
	\> \>   $(\ext k \dr k \ge j \rb (\sigma,k) \models q \land (\all i \dr j\le i < k \rb (\sigma,i) \models p))$\\[\lgap]
	\> $=$  \>  \Hint{Case $k=j$}\\[\lgap]
	\> \>   $(\ext k \dr k=j \rb (\sigma,k) \models q \land (\all i \dr j\le i < j \rb (\sigma,i) \models p))$\\[\lgap]
	\> $=$  \>  \Hint{$j\le i < j \equiv false$}\\[\lgap]
	\> \>   $(\ext k \dr k=j \rb (\sigma,k) \models q \land (\all i \dr false \rb (\sigma,i) \models p))$\\[\lgap]
	\> $=$  \>  \Hint{(8.13) Empty range rule $(\star x \dr false \rb P) =u$ with $true$ the identity of $\land$}\\[\lgap]
	\> \>   $(\ext k \dr k=j \rb (\sigma,k) \models q \land true$)\\[\lgap]
	\> $=$  \>  \Hint{(3.39) Identity of $\land$, $p \land true \equiv p$}\\[\lgap]
	\> \>   $(\ext k \dr k=j \rb (\sigma,k) \models q$)\\[\lgap]
	\> $=$  \>  \Hint{(8.14) One-point rule $(\star x\dr x=E\rb P) = P[x:=E]$}\\[\lgap]
	\> \>   $((\sigma,k) \models q)[k := j]$\\[\lgap]
	\> $=$  \>  \Hint{Textual substitution}\\[\lgap]
	\> \>   $(\sigma,j) \models q$\\[\lgap]
	\> $=$  \>  \Hint{Case $q$ holds in state $s_j$}\\[\lgap]
	\> \>   $true$ \quad \myqed
\end{tabbing}
This result is theorem (\ref{E:zeroUntil}) $p \Until true \equiv true$ proved in Section \ref{section-until}.
$true$ is the right zero of the \textit{until} operator.

The \textit{until} operator $\Until$ is not associative as shown by the following sequence.\\[\lllgap]
\begin{tabular}{c|cccccccc}
  $\sigma$                  & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & \dots \\
  \hline
  $p$                       & F     & T     & F     & T     & F     &  \dots\\
  $q$                       & F     & F     & T     & F     & T     &  \dots\\
  $r$                       & F     & F     & F     & F     & T     &  \dots\\
  $p\Until q$               & F     & T     & T     & T     & T     &  \dots\\
  $q\Until r$               & F     & F     & F     & F     & T     &  \dots\\
  $p\Until (q\Until r)$     & F     & F     & F     & T     & T     &  \dots\\
  $(p\Until q)\Until r$     & F     & T     & T     & T     & T     &  \dots
\end{tabular}\\[\lllgap]
States $s_1$ and $s_2$ in the last two rows of the above table are counterexamples, because the two expressions differ in these states.

\subsubsection*{The \textit{eventually} operator $\Event$}

The semantics of the unary prefix operator $\Event$ are
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\sigma, j) \models \Event p$ \quad iff \quad $(\ext k \dr k \ge j \rb (\sigma,k) \models p)$
\end{tabbing}
So, $\Event p$ holds in state $s_j$ if $p$ holds in state $s_j$ or in any other state $s_k$ where $k\ge j$, that is, if $p$ holds in the current state or in any other future state.

For example, suppose $x$ evolves in the computation as follows.\\[\lllgap]
\begin{tabular}{c|cccccccc}
  $\sigma$                  & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & $s_5$ & $s_6$ & \dots \\
  \hline
  $x$                       & 1     & 2     & 3     & 4     & 5     & 6     & 7     &  \dots\\
  $3\le x<6$                & F     & F     & T     & T     & T     & F     & F     &  \dots\\
  $\Event(3\le x<6)$        & T     & T     & T     & T     & T     & F     & F     &  \dots\\
\end{tabular}\\[\lllgap]
The bottom row shows the evaluation of the expression $\Event p$ where $p\equiv 3\le x<6$.
In states $s_0$ and $s_1$, $\Event p$ is true because there is a state, either now or in the future, in which $p$ will hold.

If $\Event p$ is ever false in any state $s_i$ in a sequence $\sigma$, it must be false in all subsequent states $s_j$, $j\ge i$.
If $\Event p$ is ever true in any state $s_i$ in a sequence $\sigma$, it must be true in all preceding states $s_j$, $j\le i$.
For example, suppose $p$ and $q$ evolve in the computation as follows.\\[\lllgap]
\begin{tabular}{c|ccccccccccc}
  $\sigma$       & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & $s_5$ & $s_6$ & $s_7$ & $s_8$& $s_9$  & \dots \\
  \hline
  $p$            & F     & F     & T     & F     & F     & T     & F     & F     & F     & F     &  \dots\\
  $q$            & F     & F     & T     & T     & F     & F     & T     & T     & F     & F     &  \dots\\
  $\Event p$     & T     & T     & T     & T     & T     & T     & F     & F     & F     & F     &  \dots\\
  $\Event q$     & T     & T     & T     & T     & T     & T     & T     & T     & T     & T     &  \dots\\
\end{tabular}\\[\lllgap]
The bottom two rows show the evaluation of the expressions $\Event p$ and $\Event q$
assuming that $p$ remains false indefinitely and $q$ continues to switch between true and false indefinitely.

The \textit{eventually} operator is a special case of the \textit{until} operator.
Namely, $true \Until q$ is equivalent to $\Event q$.

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
	\> \>   $(\sigma, j) \models true\Until q$\\[\lgap]
	\> $=$  \>  \Hint{Semantics of $p\Until q$ with $p:=true$}\\[\lgap]
	\> \>   $(\ext k \dr k \ge j \rb (\sigma,k) \models q \land (\all i \dr j\le i < k \rb (\sigma,i) \models true))$\\[\lgap]
	\> $=$  \>  \Hint{$true$ holds in all states}\\[\lgap]
	\> \>   $(\ext k \dr k \ge j \rb (\sigma,k) \models q \land (\all i \dr j\le i < k \rb true))$\\[\lgap]
	\> $=$  \>  \Hint{(9.8) $(\all x\dr R\rb true)\equiv true$}\\[\lgap]
	\> \>   $(\ext k \dr k \ge j \rb (\sigma,k) \models q \land true)$\\[\lgap]
	\> $=$  \>  \Hint{(3.39) Identity of $\land$, $p \land true \equiv p$}\\[\lgap]
	\> \>   $(\ext k \dr k \ge j \rb (\sigma,k) \models q)$\\[\lgap]
	\> $=$  \>  \Hint{Semantics of $\Event q$}\\[\lgap]
	\> \>   $(\sigma, j) \models \Event q$ \quad \myqed
\end{tabbing}
This relationship is the basis of the definition of $\Event p$ in (\ref{E:defEvent}) $\Event p \equiv true \Until p$
assumed in Section \ref{section-event}.

\subsubsection*{The \textit{always} operator $\Always$}

The semantics of the unary prefix operator $\Always$ are
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\sigma, j) \models \Always p$ \quad iff \quad $(\all k \dr k \ge j \rb (\sigma,k) \models p)$
\end{tabbing}
So, $\Always p$ holds in state $s_j$ if $p$ holds in state $s_j$ and in all other states $s_k$ where $k\ge j$,
that is, if $p$ holds in the current state and in all other future states.

For example, suppose $x$ evolves in the computation as follows.\\[\lllgap]
\begin{tabular}{c|ccccccccccc}
  $\sigma$                      & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & $s_5$ & $s_6$ & $s_7$ & \dots \\
  \hline
  $x$                           & 1     & 2     & 3     & 4     & 5     & 6     & 7     & 8     &  \dots\\
  $x < 4 \lor x \ge 6$          & T     & T     & T     & F     & F     & T     & T     & T     &  \dots\\
  $\Always(x < 4 \lor x \ge 6)$ & F     & F     & F     & F     & F     & T     & T     & T     &  \dots\\
\end{tabular}\\[\lllgap]
The bottom row shows the evaluation of the expression $\Always p$ where $p\equiv x < 4 \lor x \ge 6$.
In states $s_3$ and $s_4$, $\Always p$ is false because $p$ does not hold in those states.
In states $s_0$, $s_1$, and $s_2$, $p$ is true. However, $\Always p$ is false in those states because $p$ does no hold
in all future states.
In states $s_5$, $s_6$, $s_7$, and subsequent states, $\Always p$ is true because $p$ holds in in those states
and in all future states as well.

If $\Always p$ is ever true in any state $s_i$ in a sequence $\sigma$, it must be true in all subsequent states $s_j$, $j\ge i$.
If $\Always p$ is ever false in any state $s_i$ in a sequence $\sigma$, it must be false in all preceding states $s_j$, $j\le i$.

For example, suppose $p$ and $q$ evolve in the computation as follows.\\[\lllgap]
\begin{tabular}{c|ccccccccccc}
  $\sigma$       & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & $s_5$ & $s_6$ & $s_7$ & $s_8$& $s_9$  & \dots \\
  \hline
  $p$            & T     & T     & F     & T     & T     & F     & T     & T     & T     & T     &  \dots\\
  $q$            & T     & T     & F     & F     & T     & T     & F     & F     & T     & T     &  \dots\\
  $\Always p$    & F     & F     & F     & F     & F     & F     & T     & T     & T     & T     &  \dots\\
  $\Always q$    & F     & F     & F     & F     & F     & F     & F     & F     & F     & F     &  \dots\\
\end{tabular}\\[\lllgap]
The bottom two rows show the evaluation of the expressions $\Always p$ and $\Always q$
assuming that $p$ remains true indefinitely and $q$ continues to switch between true and false indefinitely.

$\Always p$ is a universal operator, while $\Event p$ is an existential operator.
In the same way that $(\all x\dr R\rb P)$ is equivalent to $\neg (\ext x\dr R\rb \neg P)$ through the generalized De Morgan theorem, $\Always p$ is equivalent to $\neg\Event\neg p$.

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
	\> \>   $(\sigma, j) \models \Always p$\\[\lgap]
	\> $=$  \>  \Hint{Semantics of $\Always p$}\\[\lgap]
	\> \>   $(\all k \dr k \ge j \rb (\sigma,k) \models p)$\\[\lgap]
	\> $=$  \>  \Hint{(9.18a) Generalized De Morgan $\neg (\ext x\dr R\rb \neg P)\equiv (\all x\dr R\rb P)$}\\[\lgap]
	\> \>   $\neg (\ext k \dr k \ge j \rb \neg((\sigma,k) \models p))$\\[\lgap]
	\> $=$  \>  \Hint{$p$ does not hold in a state iff $\neg p$ holds in that state}\\[\lgap]
	\> \>   $\neg (\ext k \dr k \ge j \rb (\sigma,k) \models \neg p)$\\[\lgap]
	\> $=$  \>  \Hint{Semantics of $\Event p$}\\[\lgap]
	\> \>   $\neg ((\sigma, j) \models \Event \neg p)$\\[\lgap]
	\> $=$  \>  \Hint{$p$ does not hold in a state iff $\neg p$ holds in that state}\\[\lgap]
	\> \>   $(\sigma, j) \models \neg \Event \neg p$ \quad \myqed\\
\end{tabbing}
This relationship is the basis of the definition of $\Always p$ in equation (\ref{E:defAlways})
$\Always p \equiv \neg\Event\neg p$ assumed in Section \ref{section-always}.

The above equational proof illustrates a common advantage of $\mathcal{E}$ over traditional logic systems.
The same equivalence is proved in \cite{Ben} but only by resorting to proof by mutual implication using proof by contradiction within each case.
Gries and Schneider \cite{LADM} point out that many equivalence proofs are shorter in $\mathcal{E}$, in which equality is central, than in traditional systems, in which implication is central.

The above demonstration that $(\sigma, j) \models \Always p \equivs (\sigma, j) \models \neg \Event \neg q$ depends on the
rule, ``$p$ does not hold in a state iff $\neg p$ holds in that state'', written formally as
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $\neg ((\sigma, j) \models p)$ \quad iff \quad $(\sigma, j) \models \neg p$
\end{tabbing}
The corresponding rules for the binary operators are
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $((\sigma, j) \models p) \;\land\; ((\sigma, j) \models q)$ \quad iff \quad $(\sigma, j) \models p\land q$\\
  \> $((\sigma, j) \models p) \;\lor\; ((\sigma, j) \models q)$ \quad iff \quad $(\sigma, j) \models p\lor q$\\
  \> $((\sigma, j) \models p) \;\impl\; ((\sigma, j) \models q)$ \quad iff \quad $(\sigma, j) \models p \impl q$\\
  \> $((\sigma, j) \models p) \;\equiv\; ((\sigma, j) \models q)$ \quad iff \quad $(\sigma, j) \models p \equiv q$
\end{tabbing}

%One defining axiom for the \textit{always} operator that does not seem to appear in the temporal logic literature is
%(\ref{E:axiomUntilImpl}) $\Always p \land \Event q \impl p \Until q$.
%Here is a demonstration of this implication.
%
%\begin{tabbing}
%\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
%	\> \>   $(\sigma, j) \models \Always p \land \Event q$\\[\lgap]
%	\> $=$  \>  \Hint{$((\sigma, j) \models p) \;\land\; ((\sigma, j) \models q)$ iff $(\sigma, j) \models p\land q$}\\[\lgap]
%	\> \>   $((\sigma, j) \models \Always p) \;\land\; ((\sigma, j) \models \Event q)$\\[\lgap]
%	\> $=$  \>  \Hint{Semantics of $\Always p$ and $\Event q$}\\[\lgap]
%	\> \>   $(\all i \dr i \ge j \rb (\sigma, i) \models p) \land (\ext k \dr  k \ge j \rb (\sigma, k) \models q)$\\[\lgap]
%	\> $=$  \>  \Hintfirst{(9.21) Distributivity of $\land$ over $\ext$, $P\land (\ext x \dr R \rb Q) \equiv (\ext x \dr R \rb P\land Q)$}\\[\lgap]
%	\>      \>  \Hintlast{as $\neg occurs(\Lq k\Rq ,\Lq (\all i \dr i \ge j \rb (\sigma, i) \models p) \Rq)$}\\[\lgap]
%	\> \>   $(\ext k \dr  k \ge j \rb (\sigma, k) \models q\land (\all i \dr i \ge j \rb (\sigma, i) \models p))$\\[\lgap]
%	\> $=$  \>  \Hint{$i \ge j \equiv j\le i < k\lor k\le i$}\\[\lgap]
%	\> \>   $(\ext k \dr  k \ge j \rb (\sigma, k) \models q\land (\all i \dr j\le i < k\lor k\le i \rb (\sigma, i) \models p))$\\[\lgap]
%	\> $=$  \>  \Hint{(8.18) Range split $(\star x \dr R \lor S \rb P) = (\star x \dr R \rb P) \star (\star x \dr S \rb P)$}\\[\lgap]
%	\> \>   $(\ext k \dr  k \ge j \rb (\sigma, k) \models q\land (\all i \dr j\le i < k\rb (\sigma, i) \models p)\land (\all i \dr k\le i \rb (\sigma, i) \models p))$\\[\lgap]
%	\> $\impl$  \>  \Hintfirst{(3.76b) $p\land q\impl p$ and (9.27) Monotonicity of $\ext$}\\[\lgap]
%	\>      \>  \Hintlast{$(\all x\dr R\rb Q\impl P)\impl ((\ext x\dr R\rb Q)\impl (\ext x\dr R\rb P))$}\\[\lgap]
%	\> \>   $(\ext k \dr  k \ge j \rb (\sigma, k) \models q\land (\all i \dr j\le i < k\rb (\sigma, i) \models p)$\\[\lgap]
%	\> $=$  \>  \Hint{Semantics of $\Until$}\\[\lgap]
%	\> \>   $(\sigma, j) \models p\Until q$\\[\lgap]
%\end{tabbing}

One defining axiom for the \textit{always} operator that does not seem to appear in the temporal logic literature is
$p\Until \Always q\impl \Always (p\Until q)$.

\emph{Proof}:
Expanding $p\Until \Always q$,
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
	\> \>   $(\sigma,j) \models p\Until \Always q$\\[\lgap]
	\> $=$  \>  \Hint{Semantics of $\Until$}\\[\lgap]
	\> \>   $(\ext k \dr k\ge j \rb (\sigma,k) \models \Always q \land (\all i \dr j\le i < k \rb (\sigma, i) \models p))$\\[\lgap]
	\> $=$  \>  \Hint{Semantics of $\Always$}\\[\lgap]
	\> \>   $(\ext k \dr k\ge j \rb (\all m \dr m\ge k \rb (\sigma, m) \models q) \land (\all i \dr j\le i < k \rb (\sigma, i) \models p))$
\end{tabbing}

\begin{figure}[t]
\centering
\begin{picture}(360,110)
\thicklines
\put(0,90)  {\vector(1,0){360}}
\put(20,90) {\circle*{8}} \put(180,90) {\circle*{8}}
\put(18,76)  {$j$} \put(178,76)  {$k$}
\put(168,64) {$k\ge j$}
\put(180,42) {\vector(1,0){180}}
\put(180,42) {\circle*{8}}
\put(240,48) {$(\sigma,m)\models q$}
\put(250,32) {$m\ge k$}
\put(20,10)  {\line(1,0){156}}
\put(20,10)  {\circle*{8}} \put(180,10) {\circle{8}}
\put(80,18) {$(\sigma,i)\models p$}
\put(80,0) {$j\le i < k$}
\end{picture}
\caption{The temporal segments for which $p$ and $q$ hold for $p\Until \Always q$.
\label{temporal-segments-until-always}}
\end{figure}

Figure \ref{temporal-segments-until-always} illustrates the temporal segments for which $p$ and $q$ hold for $p\Until \Always q$.
To prove that $p\Until \Always q\impl \Always (p\Until q)$ it suffices to show that $p\Until q$ holds for all time greater than or equal to $j$,
given that $p$ and $q$ hold as above.

Case 1. $\quad p\Until q$ holds at $(\sigma,i)$ for $j\le i \le k$.\\
$p\Until q$ holds in this case, because $p$ holds at $(\sigma,i)$ for $j\le i < k$, and $q$ holds at $(\sigma,k)$.

Case 2. $\quad p\Until q$ holds at $(\sigma,m)$ for $m>k$.\\
$p\Until q$ holds in this case, because $q$ holds at $(\sigma,m)$ for $m\ge k$, and $true$ is the right zero of $\Until$.

From Case 1 and Case 2, $p\Until q$ holds at $(\sigma,i)$ for $i\ge j$. \quad \myqed

\subsubsection*{The \textit{wait} operator $\Wait$}

The semantics of the binary infix operator $\Wait$ in terms of $\Until$ and $\Always$ are
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> $(\sigma, j) \models p \Wait q$ \quad iff \quad $(\sigma, j) \models p \Until q \; \lor \; (\sigma, j) \models \Always p$
\end{tabbing}
The \textit{wait} operator $\Wait$ is weaker than the \textit{until} operator $\Until$, because $p\Wait q$ does not require $q$ to ever be true,
while $p\Until q$ does.

For example, suppose $p$ and $q$ evolve in the computation as follows.\\[\lllgap]
\begin{tabular}{c|cccccccccccc}
  $\sigma$       & $s_0$ & $s_1$ & $s_2$ & $s_3$ & $s_4$ & $s_5$ & $s_6$ & $s_7$ & $s_8$& $s_9$  & $s_{10}$&  \dots \\
  \hline
  $p$            & F     & F     & T     & T     & F     & F     & F     & F     & T     & T     & T     &  \dots\\
  $q$            & F     & F     & F     & F     & T     & T     & F     & F     & F     & F     & F     &  \dots\\
  $\Always p$    & F     & F     & F     & F     & F     & F     & F     & F     & T     & T     & T     &  \dots\\
  $p\Until q$    & F     & F     & T     & T     & T     & T     & F     & F     & F     & F     & F     &  \dots\\
  $p\Wait q$     & F     & F     & T     & T     & T     & T     & F     & F     & T     & T     & T     &  \dots\\
\end{tabular}\\[\lllgap]
The bottom two rows show the evaluation of the expressions $p\Until q$ and $p\Wait q$
assuming that $p$ remains true indefinitely and $q$ remains false indefinitely.
From $s_0$ to $s_7$, $p\Until q$ and $p\Wait q$ hold in the same states.
From $s_8$ on, however, $p\Until q$ does not hold because $q$ never holds thereafter,
while $p\Wait q$ does hold because $p$ always holds thereafter.

\section{The Equational Temporal System}

This section presents an axiomatic deductive system of temporal logic and proves its theorems with the equational
logic $\mathcal{E}$ of Gries and Schneider \cite{LADM} (LADM).
Theorems cited in a proof hint take two forms.
A numbered reference enclosed in parentheses \textit{without} a period is a reference to an axiom or a previously-proved
theorem in this paper.
A numbered reference enclosed in parentheses \textit{with} a period is a reference to an axiom or a
theorem from the propositional calculus in LADM.
The numbering is consistent with that text with the chapter number followed by the equation number separated by the period.
Additional theorems, either not included in LADM or included but not numbered, are indicated by a three-part number with two period separators.
The terms ``definition'' and ``axiom'' are synonymous.

The propositional calculus theorems from LADM, together with a listing of the theorems of this paper, are included in a companion document. \cite{vegaTheorems}
The following exposition includes the theorems from LADM in the proof hints, except that theorems are omitted for (4.2) and (4.3) Monotonicity, as they are described in Section \ref{sec-equational-deductive-systems}.

\subsection{Next}\label{section-next}

The following two axioms define the \textit{next} operator $\Next$.
\begin{equation}\label{E:selfDual}
\textbf{Axiom, Self-dual:}\quad \Next\neg p \equiv \neg\Next p
\end{equation}
\begin{equation}\label{E:distNextImp}
\textbf{Axiom, Distributivity of $\Next$ over $\impl$:}\quad \Next (p \impl q) \equiv \Next p \impl \Next q
\end{equation}

Self duality states that $p$ not holding in the next state is equivalent to \textit{next} $p$ not holding in the current state.
Neither of the other unary temporal operators, \textit{eventually} $\Event$ nor \textit{always} $\Always$, are equivalent to their duals.
The \textit{next} operator describes the state fixed at one step into the future.
In contrast, $\Event$ and $\Always$ describe sequences of states arbitrarily far into the future.

Distributivity states that $p$ implies $q$ in the next state is equivalent to \textit{next} $p$ implies \textit{next} $q$ in the current state.
From this axiom, subsequent theorems prove that the \textit{next} operator distributes over all the propositional binary operators.

Linearity follows from self-dual and distributivity of $\Next$ over $\impl$.
\begin{equation}\label{E:linearity}
\textbf{Linearity:}\quad \Next p \equiv \neg\Next\neg p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Next p \equiv \neg\Next\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(3.11) $\neg p \equiv q \equiv p \equiv \neg q$ with $p,q := \Next\neg p, \Next p$} \\[\lgap]
  \> \>   $\neg\Next p \equiv \Next\neg p$ \\[\lgap]
  \> which is (\ref{E:selfDual}), Self-dual. \quad \myqed
\end{tabbing}

Here are proofs that $\Next$ distributes over $\lor$, $\land$, and $\equiv$.
\begin{equation}\label{E:distNextOr}
\textbf{Distributivity of $\Next$ over $\lor$:}\quad \Next (p \lor q) \equiv \Next p \lor \Next q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
	\> \>   $\Next(p \lor q)$\\[\lgap]
	\> $=$  \>  \Hint{(3.59) Implication $p\impl q \equivs \neg p \lor q$}\\[\lgap]
	\> \>   $\Next(\neg p \impl q)$\\[\lgap]
	\> $=$  \>  \Hint{(\ref{E:distNextImp}) Distributivity of $\Next$ over $\impl$}\\[\lgap]
	\> \>   $\Next\neg p \impl \Next q$\\[\lgap]
	\> $=$  \>  \Hint{(3.59) Implication $p\impl q \equivs \neg p \lor q$ with $p,q := \Next\neg p, \Next q$}\\[\lgap]
	\> \>   $\neg\Next\neg p \lor \Next q$\\[\lgap]
	\> $=$  \>  \Hint{(\ref{E:linearity}) Linearity}\\[\lgap]
	\> \>   $\Next p \lor \Next q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:distNextAnd}
\textbf{Distributivity of $\Next$ over $\land$:}\quad \Next (p \land q) \equiv \Next p \land \Next q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Next (p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$, twice}\\[\lgap]
  \> \>   $\Next (\neg\neg p \land \neg\neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.47b) De Morgan, $\neg (p \lor q) \equiv \neg p \land \neg q$}\\[\lgap]
  \> \>   $\Next\neg(\neg p \lor \neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:selfDual}) Self-dual with $p:= (\neg p \lor \neg q$)}\\[\lgap]
  \> \>   $\neg\Next (\neg p \lor \neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distNextOr}) Distributivity of $\Next$ over $\lor$ with $p,q := \neg p, \neg q$}\\[\lgap]
  \> \>   $\neg (\Next\neg p \lor \Next \neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:selfDual}) Self-dual twice}\\[\lgap]
  \> \>   $\neg(\neg\Next p \lor \neg\Next q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.47a) De Morgan $\neg (p \land q) \equiv \neg p \lor \neg q$}\\[\lgap]
  \> \>   $\neg\neg(\Next p \land \Next q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$}\\[\lgap]
  \> \>   $\Next p \land \Next q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:distNextEquiv}
\textbf{Distributivity of $\Next$ over $\equiv$:}\quad \Next (p \equiv q) \equiv \Next p \equiv \Next q
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Next (p \equiv q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.80) Mutual implication $(p\impl q) \land (q\impl p) \equivs (p\equiv q)$}\\[\lgap]
  \> \>   $\Next ((p \impl q) \land (q \impl p))$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distNextAnd}) Distributivity of $\Next$ over $\land$}\\[\lgap]
  \> \>   $\Next (p \impl q) \land \Next (p \impl q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distNextImp}) Distributivity of $\Next$ over $\impl$}\\[\lgap]
  \> \>   $(\Next p \impl \Next q) \land (\Next q \impl \Next p)$\\[\lgap]
  \> $=$  \>  \Hint{(3.80) Mutual Implication $(p\impl q) \land (q\impl p) \equivs (p\equiv q)$}\\[\lgap]
  \> \>   $\Next p \equiv \Next q$ \quad \myqed
\end{tabbing}
}

\opt{student}{
Exercise for the student. Hint: Start with mutual implication.\\
}

Now, $true$ holds in the next state, and $false$ does not hold in the next state.
Theorems (\ref{E:nextTruth}) and (\ref{E:nextFalse}) are unique to this system.
In the equational logic of LADM, $true$ is theorem (3.4) and is equivalent to all other theorems.
Theorem (\ref{E:nextTruth}) shows that all propositional logic theorems hold at the next state
and, by induction, hold at all states.
\begin{equation}\label{E:nextTruth}
\textbf{Truth of $\Next$:}\quad \Next true \equiv true
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
	\> \>   $\Next true$\\[\lgap]
	\> $=$  \>  \Hint{(3.28) Excluded middle $p\lor\neg p$}\\[\lgap]
	\> \>   $\Next(p \lor \neg p)$\\[\lgap]
	\> $=$  \>  \Hint{(\ref{E:distNextOr}) Distributivty of $\Next$ over $\lor$}\\[\lgap]
	\> \>   $\Next p \lor \Next\neg p$\\[\lgap]
	\> $=$  \>  \Hint{(\ref{E:selfDual}) Self-dual}\\[\lgap]
	\> \>   $\Next p \lor \neg\Next p$\\[\lgap]
	\> $=$  \>  \Hint{(3.28) Excluded middle $p\lor\neg p$ with $p := \Next p$}\\[\lgap]
	\> \>   $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:nextFalse}
\textbf{Falsehood of $\Next$:}\quad \Next false \equiv false
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Next false \equiv false$\\[\lgap]
  \> $=$  \>  \Hint{(3.8) Definition of $false$, $false\equiv \neg true$} \\[\lgap]
  \> \>   $\Next\neg true \equiv \neg true$\\[\lgap]
  \> $=$  \>  \Hint{(3.11) $\neg p \equiv q \equiv p \equiv \neg q$ with $p,q := true, \Next\neg true$}\\[\lgap]
  \> \>   $\neg\Next\neg true \equiv true$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:linearity}) Linearity}\\[\lgap]
  \> \>   $\Next true \equiv true$\\[\lgap]
  \> which is (\ref{E:nextTruth}) Truth of $\Next$. \quad \myqed
\end{tabbing}
}

\opt{student}{
Exercise for the student.\\
}

\subsection{Until}\label{section-until}

This system defines the \textit{until} operator $\Until$ with the following nine axioms.
The distributivity of \textit{next} over \textit{until} (\ref{E:distNextUntil}) implies the distributivity of \textit{next} over \textit{wait} as Section \ref{section-wait} shows.
Thus \textit{next} distributes over all binary operators, both propositional and temporal.

The \textit{until} operator is unlike any propositional binary operator.
Its right operand has an existential characteristic and its left operand has a universal characteristic.
Expansion (\ref{E:expansionUntil}) states that
$p\Until q$ is true iff $q$ is true in the current state, or $p$ is true in the current state and $p\Until q$ is
true in the next state.
Thus, $q$ relates to the definition through disjunction, which is existential,
while $p$ relates through conjunction, which is universal.
Consequently, the \textit{until} operator is neither symmetric (\textit{i.e.} commutative) nor associative.
\begin{equation}\label{E:distNextUntil}
\textbf{Axiom, Distributivity of $\Next$ over $\Until$:}\quad \Next (p \Until q) \equiv \Next p \Until \Next q
\end{equation}

\firstspacer

\begin{equation}\label{E:expansionUntil}
\textbf{Axiom, Expansion of $\Until$:}\quad p \Until q \equiv q \lor (p \land \Next (p \Until q))
\end{equation}

\firstspacer

\begin{equation}\label{E:untilFalse}
\textbf{Axiom, Right zero of $\Until$:}\quad p \Until false \equiv false
\end{equation}

The following four axioms describe how the \textit{until} operator distributes over conjunction and disjunction.
Because $\Until$ is not symmetric, this system requires separate axioms for left and right distributivity.
\begin{equation}\label{E:untilOrEquiv}
\textbf{Axiom, Left distributivity of $\Until$ over $\lor$ :}\quad p \Until (q \lor r) \equiv p \Until q \lor p \Until r
\end{equation}

\firstspacer

\begin{equation}\label{E:untilOrImp}
\textbf{Axiom, Right distributivity of $\Until$ over $\lor$ :}\quad p \Until r \lor q \Until r \impl (p \lor q) \Until r
\end{equation}

\firstspacer

\begin{equation}\label{E:untilAndImp}
\textbf{Axiom, Left distributivity of $\Until$ over $\land$ :}\quad p \Until (q \land r) \impl p \Until q \land p \Until r
\end{equation}

\firstspacer

\begin{equation}\label{E:untilAndEquiv}
\textbf{Axiom, Right distributivity of $\Until$ over $\land$ :}\quad (p \land q) \Until r \equiv p \Until r \land q \Until r
\end{equation}

The following two axioms are the absorption laws of the \textit{until} operator.
All systems have these two absorption theorems, because the \textit{until} operator is not associative.
Manna and Pnueli \cite{Manna} refer to these as idempotence properties.
This paper follows Schneider \cite{Schn}, which refers to them as absorption properties.
\begin{equation}\label{E:untilIdem}
\textbf{Axiom, Left absorption of $\Until$:}\quad p \Until (p \Until q) \equiv p \Until q
\end{equation}

\firstspacer

\begin{equation}\label{E:untilIdemR}
\textbf{Axiom, Right absorption of $\Until$:}\quad (p \Until q) \Until q \equiv p \Until q
\end{equation}

Theorem (\ref{E:untilExcludedMiddle}) is the \textit{until} version of excluded middle.
Theorem (\ref{E:idemUntil}) shows that the \textit{until} operator is idempotent.
Theorem (\ref{E:zeroUntil}) shows that $true$ is a right zero of $\Until$, which is unusual because
axiom (\ref{E:untilFalse}) shows that $false$ is also a right zero of $\Until$.
\begin{equation}\label{E:untilExcludedMiddle}
\Until \textbf{excluded middle:}\quad p \Until q \lor p\Until \neg q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Until q \lor p\Until \neg q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionUntil}) Expansion, twice} \\[\lgap]
\> \> $q\lor (p\land \Next (p\Until q))\lor \neg q \lor (p\land \Next (p\Until \neg q))$\\[\lgap]
\> $=$ \> \Hint{(3.28) Excluded middle, $p\lor \neg p$} \\[\lgap]
\> \> $true \lor (p\land \Next (p\Until q)) \lor (p\land \Next (p\Until \neg q))$\\[\lgap]
\> $=$ \> \Hint{(3.29) Zero of $\lor$, $p\lor true\equiv true$} \\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:idemUntil}
\textbf{Idempotency of $\Until$:}\quad p \Until p \equiv p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $p \lor (p \land \Next(p \Until p))$\\[\lgap]
  \> $=$  \>  \Hint{(3.43b) Absorption, $p \lor (p \land q) \equiv p$ with $q := \Next (p \Until p)$}\\[\lgap]
  \> \>   $p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:zeroUntil}
\textbf{Right zero of $\Until$:}\quad p \Until true \equiv true
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until true$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $true \lor (p \land \Next(p \Until true))$\\[\lgap]
  \> $=$  \>  \Hint{(3.29) Zero of $\lor$, $p\lor true\equiv true$}\\[\lgap]
  \> \>   $true$ \quad \myqed
\end{tabbing}
}

\opt{student}{
Exercise for the student.\\
}

Theorem (\ref{E:leftIdUntil}) shows that $false$ is the left identity of $\Until$.
Theorems (\ref{E:untilFalse}), (\ref{E:zeroUntil}), and (\ref{E:leftIdUntil}) cover three of the
possibilities of constants $true$ and $false$ on either side of $\Until$.
None of these three theorems seem to appear in the temporal logic literature.
The fourth possibility with $true$ as the left argument is the basis of the definition of the \textit{eventually}
operator $\Event$ in Section \ref{section-event}.
\begin{equation}\label{E:leftIdUntil}
\textbf{Left identity of $\Until$:}\quad false \Until q \equiv q
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $false \Until q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $q \lor (false \land \Next(false \Until q))$\\[\lgap]
  \> $=$  \>  \Hint{(3.40) Zero of $\land$, $p\land false\equiv false$}\\[\lgap]
  \> \>   $q \lor false$\\[\lgap]
  \> $=$  \>  \Hint{(3.30) Identity of $\lor$, $p\lor false\equiv p$}\\[\lgap]
  \> \>   $q$ \quad \myqed
\end{tabbing}
}

\opt{student}{
Exercise for the student.\\
}

Theorem (\ref{E:untilImpOr}) is interesting because it relates the temporal expression on the left hand side
to the propositional expression on the right hand side.
\begin{equation}\label{E:untilImpOr}
p \Until q \impl p \lor q
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $q \lor (p \land \Next(p \Until q))$\\[\lgap]
  \> $\impl$  \>  \Hint{(3.76d) $p\lor (q\land r) \impl p\lor q$ with $p,q,r := q,p,\Next(p \Until q)$}\\[\lgap]
  \> \>   $p \lor q$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:untilInsertion}
\textbf{Insertion:}\quad q \impl p \Until q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$} \\[\lgap]
\> \> $q \lor (p \land \Next(p \Until q))$\\[\lgap]
\> $\foll$ \> \Hint{(3.76a) Weakening, $p\impl p\lor q$} \\[\lgap]
\> \> $q$ \quad \myqed
\end{tabbing}

This system has the following five additional absorption properties that do not seem to
appear in the temporal logic literature.
\begin{equation}\label{E:untilOrP}
\textbf{Absorption:}\quad p \lor p \Until q \equiv p \lor q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \lor p \Until q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $p \lor q \lor (p \land \Next(p \Until q))$\\[\lgap]
  \> $=$  \>  \Hint{(3.43b) Absorption $p \lor (p \land q) \equiv p$}\\[\lgap]
  \> \>   $p \lor q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:untilOrQ}
\textbf{Absorption:}\quad p \Until q \lor q \equiv p \Until q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until q \lor q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $q \lor (p \land \Next(p \Until q)) \lor q$\\[\lgap]
  \> $=$  \>  \Hint{(3.26) Idempotency of $\lor$, $p \lor p \equiv p$}\\[\lgap]
  \> \>   $q \lor (p \land \Next(p \Until q))$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $p \Until q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:untilAndQ}
\textbf{Absorption:}\quad p \Until q \land q \equiv q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until q \land q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $(q \lor (p \land \Next(p \Until q))) \land q$\\[\lgap]
  \> $=$  \>  \Hint{(3.43a) Absorption $p \land (p \lor q) \equiv p$}\\[\lgap]
  \> \>   $q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:untilAndOr}
\textbf{Absorption:}\quad p \Until q \land (p \lor q) \equiv p \Until q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until q \land (p \lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $(q \lor (p \land \Next(p \Until q))) \land (p \lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.45) Distributivity of $\lor$ over $\land$, $p\lor (q\land r)\equiv (p\lor q)\land (p\lor r)$}\\[\lgap]
  \> \>   $q \lor (p \land p \land \Next(p \Until q))$\\[\lgap]
  \> $=$  \>  \Hint{(3.38) Idempotency of $\land$, $p \land p \equiv p$}\\[\lgap]
  \> \>   $q \lor (p \land \Next(p \Until q))$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $p \Until q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:untilOrAnd}
\textbf{Absorption:}\quad p \Until q \lor (p \land q) \equiv p \Until q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until q \lor (p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $q \lor (p \land \Next(p \Until q)) \lor (p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.43b) Absorption, $p \lor (p \land q) \equiv p$}\\[\lgap]
  \> \>   $q \lor (p \land \Next(p \Until q))$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $p \Until q$ \quad \myqed
\end{tabbing}

\subsection{Eventually}\label{section-event}

Eventually $\Event$ is a special case of $\Until$ when the left hand side is $true$.
Equation (\ref{E:defEvent}) is its only defining axiom.
\begin{equation}\label{E:defEvent}
\textbf{Definition of $\Event$:}\quad \Event q \equiv true \Until q
\end{equation}

The following theorem shows how the unary operator \textit{eventually} absorbs into the binary operator \textit{until}.
\begin{equation}\label{E:absEventIntoUntil}
\textbf{Absorption of $\Event$ into $\Until$:}\quad p \Until q\land \Event q \equiv p\Until q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until q\land \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $p \Until q\land true\Until q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilAndEquiv}) Right distributivity of $\Until$ over $\land$}\\[\lgap]
  \> \>   $(p\land true) \Until q$\\[\lgap]
  \> $=$  \>  \Hint{(3.39) Identity of $\land$, $p\land true\equiv p$}\\[\lgap]
  \> \>   $p\Until q$ \quad \myqed
\end{tabbing}

$p\Until q$ guarantees that $q$ will eventually be $true$ as follows.
\begin{equation}\label{E:eventuality}
\textbf{Eventuality:}\quad p \Until q \impl \Event q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absEventIntoUntil})Absorption of $\Event$ into $\Until$}\\[\lgap]
  \> \>   $p \Until q \land \Event q$\\[\lgap]
  \> $\impl$  \>  \Hint{(3.76b) Strengthening the antecedent, $p\land q \impl p$}\\[\lgap]
  \> \>   $\Event q$ \quad \myqed
\end{tabbing}

Theorems (\ref{E:eventTrue}) and (\ref{E:eventFalse}), Truth and Falsehood of $\Event$, are unique to this system.
\begin{equation}\label{E:eventTrue}
\textbf{Truth of $\Event$:}\quad \Event true \equiv true
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event true$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $true \Until true$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:idemUntil}) Idempotency of $\Until$}\\[\lgap]
  \> \>   $true$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:eventFalse}
\textbf{Falsehood of $\Event$:}\quad \Event false \equiv false
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event false$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $true \Until false$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilFalse}) Right zero of $\Until$}\\[\lgap]
  \> \>   $false$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

Expansion of $\Event$, like expansion of $\Until$, has two disjuncts.
The first describes the current state and the second contains the operation in the next state.
\begin{equation}\label{E:expansionEvent}
\textbf{Expansion of $\Event$:}\quad \Event p \equiv p \lor \Next\Event p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $true \Until p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
  \> \>   $p \lor (true \land \Next(true \Until p))$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $p \lor (true \land \Next\Event p)$\\[\lgap]
  \> $=$  \>  \Hint{(3.39) Identity of $\land$, $p\land true\equiv p$}\\[\lgap]
  \> \>   $p \lor \Next\Event p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

The following two absorption theorems do not seem to appear in the temporal logic literature.
\begin{equation}\label{E:absOrIntoEvent}
\textbf{Absorption of $\lor$ into $\Event$:}\quad p \lor \Event p \equiv \Event p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \lor \Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionEvent}) Expansion of $\Event$}\\[\lgap]
  \> \>   $p \lor p \lor \Next\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(3.26) Idempotency of $\lor$, $p\lor p \equiv p$}\\[\lgap]
  \> \>   $p \lor \Next\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionEvent}) Expansion of $\Event$}\\[\lgap]
  \> \>   $\Event p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:absEventIntoAnd}
\textbf{Absorption of $\Event$ into $\land$:}\quad \Event p \land p \equiv p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event p \land p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionEvent}) Expansion of $\Event$}\\[\lgap]
  \> \>   $(p \lor \Next\Event p) \land p$\\[\lgap]
  \> $=$  \>  \Hint{(3.43a) Absorption, $p\land (p \lor q) \equiv p$}\\[\lgap]
  \> \>   $p$ \quad \myqed
\end{tabbing}

The following six theorems for $\Event$ are common to all temporal logic systems.
\begin{equation}\label{E:impEvent}
\textbf{Weakening of $\Event$:}\quad p \impl \Event p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionEvent}) Expansion of $\Event$}\\[\lgap]
  \> \>   $p \lor \Next\Event p$\\[\lgap]
  \> $\foll$  \>  \Hint{(3.76a) Weakening the consequent, $p \impl p\lor q$}\\[\lgap]
  \> \>   $p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:nextEvent}
\textbf{Weakening of $\Event$:}\quad \Next p \impl \Event p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionEvent}) Expansion of $\Event$}\\[\lgap]
  \> \>   $p \lor \Next\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionEvent}) Expansion of $\Event$}\\[\lgap]
  \> \>   $p \lor \Next (p \lor \Next\Event p)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distNextOr}) Distributivity of $\Next$ over $\lor$}\\[\lgap]
  \> \>   $p \lor \Next p \lor \Next\Next\Event p$\\[\lgap]
  \> $\foll$  \>  \Hint{(3.76a) Weakening the consequent, $p \impl p\lor q$}\\[\lgap]
  \> \>   $\Next p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:IdemEvent}
\textbf{Absorption of $\Event$:}\quad \Event\Event p \equiv \Event p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$, with $p := \Event p$}\\[\lgap]
  \> \>   $true \Until \Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $true \Until (true \Until p)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilIdem}) Left absorption of $\Until$ with $p,q := true,p$}\\[\lgap]
  \> \>   $true \Until p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $\Event p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:dNextEvent}
\textbf{Exchange of $\Next$ and $\Event$:}\quad \Next\Event p \equiv \Event\Next p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Next\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $\Next(true \Until p)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distNextUntil}) Distributivity of $\Next$ over $\Until$}\\[\lgap]
  \> \>   $\Next true \Until \Next p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:nextTruth}) Truth of $\Next$}\\[\lgap]
  \> \>   $true \Until \Next p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $\Event\Next p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:distEventOr}
\textbf{Distributivity of $\Event$ over $\lor$:}\quad \Event(p \lor q) \equiv \Event p \lor \Event q
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event(p \lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $true \Until (p \lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilOrEquiv}) Left distributivity of $\Until$ over $\lor$}\\[\lgap]
  \> \>   $true \Until p \lor true \Until q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$ twice}\\[\lgap]
  \> \>   $\Event p \lor \Event q$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:distEventAnd}
\textbf{Distributivity of $\Event$ over $\land$:}\quad \Event(p \land q) \impl \Event p \land \Event q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event(p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $true \Until (p \land q)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:untilAndImp}) Left distributivity of $\Until$ over $\land$}\\[\lgap]
  \> \>   $true \Until p \land true \Until q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$ twice}\\[\lgap]
  \> \>   $\Event p \land \Event q$ \quad \myqed
\end{tabbing}

\subsection{Always}\label{section-always}

This system defines the \textit{always} operator $\Always$ in terms of the \textit{eventually} operator $\Event$.
$\Always p$ is true when $p$ is true in the current state and in all future states.
The defining equation (\ref{E:defAlways}) states that $p$ is always true iff it is not the case that $\neg p$ is eventually true.
\begin{equation}\label{E:defAlways}
\textbf{Definition of $\Always$:}\quad \Always p \equiv \neg\Event\neg p
\end{equation}

The following induction axiom is included in other temporal logic systems but is not used in any subsequent proofs in this system.
The $\Until\Always$ implication axiom is required to prove absorption of $\Until$ into $\Always$,
and is apparently unique to this system.
\begin{equation}\label{E:induction}
\textbf{Axiom, Induction:}\quad \Always (p \impl \Next p) \impl (p \impl \Always p)
\end{equation}

\firstspacer

\begin{equation}\label{E:axiomAlwaysUntilImpl}
\textbf{Axiom, $\Until\Always$ implication:}\quad p\Until \Always q\impl \Always (p\Until q)
\end{equation}

\firstspacer

\begin{equation}\label{E:andUntilDist}
\textbf{Axiom, Distributivity of $\land$ over $\Until$:}\quad \Always p \land q \Until r \impl (p \land q) \Until (p \land r)
\end{equation}

The following theorem shows how the binary operator \textit{until} absorbs into the unary operator \textit{always}.
\begin{equation}\label{E:absUntilAlways}
\textbf{Absorption of $\Until$ into $\Always$:}\quad p \Until \Always p \equiv \Always p
\end{equation}

\emph{Proof}: The proof is by (4.7) Mutual implication.
The proof in the first direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Until \Always p$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:axiomAlwaysUntilImpl}) $\Until\Always$ implication, with $q:=p$} \\[\lgap]
\> \> $\Always (p \Until p)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:idemUntil}) Idempotency of $\Until$} \\[\lgap]
\> \> $\Always p$
\end{tabbing}
The proof in the second direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Always p$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:untilInsertion}) Insertion, with $q:=\Always p$} \\[\lgap]
\> \> $p \Until \Always p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:axiomUntilImpl}
\textbf{$\Until$ implication:}\quad \Always p \land \Event q \impl p \Until q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p \land \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $\Always p \land true\Until q$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:andUntilDist}) Distributivity of $\land$ over $\Until$}\\[\lgap]
  \> \>   $(p \land true) \Until (p\land q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.39) Identity of $\land$, $p\land true\equiv p$}\\[\lgap]
  \> \>   $p \Until (p\land q)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:untilAndImp}) Left distributivity of $\Until$ over $\land$}\\[\lgap]
  \> \>   $p \Until p\land p\Until q$\\[\lgap]
  \> $\impl$ \> \Hint{(3.76b) Strengthening, $p\land q \impl p$} \\[\lgap]
  \> \>   $p\Until q$ \quad \myqed
\end{tabbing}

The $\Event\Always$ implication theorem states that $\Event\Always p$ ensures that $p$ will always eventually hold, but not the converse.
Suppose, for example, that $p$ continually oscillates between true and false over time.
Then, the consequent of (\ref{E:eventAlwaysImp}) is true, but the antecedent is false.
\begin{equation}\label{E:eventAlwaysImp}
\textbf{$\Event \Always$ implication:}\quad \Event\Always p \impl \Always\Event p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $true\Until \Always p$\\[\lgap]
  \> $\impl$ \> \Hint{(\ref{E:axiomAlwaysUntilImpl}) $\Until\Always$ implication}\\[\lgap]
  \> \>   $\Always (true\Until p)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $\Always\Event p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

The following theorem expresses $\Event p$ in terms of $\Always p$ and corresponds to the defining equation (\ref{E:defAlways}).
\begin{equation}\label{E:eventAsAlways}
\Event p \equiv \neg\Always\neg p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\neg\Always\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $\neg\neg\Event\neg\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$, twice}\\[\lgap]
  \> \>   $\Event p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

Whereas the \textit{next} operator $\Next$ is its own dual, the \textit{eventually} operator $\Event$
and the \textit{always} operator $\Always$
are mutually dual.
\begin{equation}\label{E:dualAlways}
\textbf{Dual of $\Always$:}\quad \neg\Always p \equiv \Event\neg p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\neg\Always p \equiv \Event\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(3.11) $\neg p \equiv q \equiv p \equiv \neg q$ with $p,q := \Always p, \Event\neg p$}\\[\lgap]
  \> \>   $\Always p \equiv \neg\Event\neg p$\\[\lgap]
  \> which is (\ref{E:defAlways}) Definition of $\Always$. \quad \myqed
\end{tabbing}
\begin{equation}\label{E:dualEvent}
\textbf{Dual of $\Event$:}\quad \neg\Event p \equiv \Always\neg p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $\neg\Event\neg\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$}\\[\lgap]
  \> \>   $\neg\Event p$ \quad \myqed
\end{tabbing}

Theorems (\ref{E:alwaysTrue}) and (\ref{E:alwaysFalse}), Truth and Falsehood of $\Always$, are unique to this system.
\begin{equation}\label{E:alwaysTrue}
\textbf{Truth of $\Always$:}\quad \Always true \equiv true
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always true$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $\neg\Event\neg true$\\[\lgap]
  \> $=$  \>  \Hint{(3.8) Definition of $false$, $false\equiv \neg true$}\\[\lgap]
  \> \>   $\neg\Event false$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:eventFalse}) Falsehood of $\Event$}\\[\lgap]
  \> \>   $\neg false$\\[\lgap]
  \> $=$  \>  \Hint{(3.13) Negation of $false$, $\neg false\equiv true$}\\[\lgap]
  \> \>   $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:alwaysFalse}
\textbf{Falsehood of $\Always$:}\quad \Always false \equiv false
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always false \equiv false$\\[\lgap]
  \> $=$  \>  \Hint{(3.8) Definition of $false$, $false\equiv \neg true$, twice}\\[\lgap]
  \> \>   $\Always\neg true \equiv \neg true$\\[\lgap]
  \> $=$  \>  \Hint{(3.11) $\neg p \equiv q \equiv p \equiv \neg q$}\\[\lgap]
  \> \>   $\neg\Always\neg\ true \equiv true$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:eventAsAlways})}\\[\lgap]
  \> \>   $\Event true \equiv true$\\[\lgap]
  \> which is (\ref{E:eventTrue}) Truth of $\Event$. \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

While the expansions of $\Until$ and $\Event$ have two disjuncts,
the expansion of $\Always$ has two conjuncts.
As usual, the first describes the current state and the second contains the operation in the next state.
\begin{equation}\label{E:expansionAlways}
\textbf{Expansion of $\Always$:}\quad \Always p \equiv p \land \Next\Always p
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $\neg\Event\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionEvent}) Expansion of $\Event$ with $p := \neg p$}\\[\lgap]
  \> \>   $\neg(\neg p\lor\Next\Event\neg p)$\\[\lgap]
  \> $=$  \>  \Hint{(3.47b) De Morgan, $\neg (p \lor q) \equiv \neg p \land \neg q$}\\[\lgap]
  \> \>   $\neg\neg p\land\neg\Next\Event\neg p)$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p \equiv p$}\\[\lgap]
  \> \>   $p\land\neg\Next\Event\neg p)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:selfDual}) Self dual}\\[\lgap]
  \> \>   $p\land\Next\neg\Event\neg p)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $p \land \Next\Always p$ \quad \myqed
\end{tabbing}

The absorption of $\land$ into $\Always$ corresponds to (\ref{E:absOrIntoEvent}) the absorption of $\lor$ into $\Event$,
while the absorption of $\Always$ into $\lor$ corresponds to (\ref{E:absEventIntoAnd}) the absorption of $\Event$ into $\land$.
Conjunction $\land$ and the \textit{always} operator $\Always$ are both universal, while
disjunction $\lor$ and the \textit{eventually} operator $\Event$ are both existential.
When the left side of the equivalence contains both existential (or both universal) operators as in (\ref{E:absOrIntoEvent}) and (\ref{E:absAndIntoAlways}),
the right side retains the same type of unary operator.
When existential and universal operators are mixed on the left side,
as in (\ref{E:absOrIntoEvent}) and (\ref{E:absAlwaysIntoOr}), the equivalence is just a statement about $p$ at the current time.
As with (\ref{E:absOrIntoEvent}) and (\ref{E:absEventIntoAnd}), the following two absorption theorems
do not seem to appear in the temporal logic literature.
\begin{equation}\label{E:absAndIntoAlways}
\textbf{Absorption of $\land$ into $\Always$:}\quad p \land \Always p \equiv \Always p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \land \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$}\\[\lgap]
  \> \>   $p \land p \land \Next \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(3.38) Idempotency of $\land$, $p\land p \equiv p$}\\[\lgap]
  \> \>   $p \land \Next \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$}\\[\lgap]
  \> \>   $\Always p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:absAlwaysIntoOr}
\textbf{Absorption of $\Always$ into $\lor$:}\quad \Always p \lor p \equiv p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p \lor p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$}\\[\lgap]
  \> \>   $(p \land \Next\Always p) \lor p$\\[\lgap]
  \> $=$  \>  \Hint{(3.43b) Absorption, $p\lor (p \land q) \equiv p$}\\[\lgap]
  \> \>   $p$ \quad \myqed
\end{tabbing}
}

\opt{student}{
Exercise for the student.\\
}

The absorption of $\Event$ into $\Always$ and of $\Always$ into $\Event$ appear to be unique to this system.
Their proofs are straightforward applications of the previous absorption theorems.
\begin{equation}\label{E:absEventIntoAlways}
\textbf{Absorption of $\Event$ into $\Always$:}\quad \Event p \land \Always p \equiv \Always p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event p \land \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absAndIntoAlways}) Absorption of $\land$ into $\Always$}\\[\lgap]
  \> \>   $\Event p \land p \land \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absEventIntoAnd}) Absorption of $\Event$ into $\land$}\\[\lgap]
  \> \>   $p \land \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absAndIntoAlways}) Absorption of $\land$ into $\Always$}\\[\lgap]
  \> \>   $\Always p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:absAlwaysIntoEvent}
\textbf{Absorption of $\Always$ into $\Event$:}\quad \Always p \lor \Event p \equiv \Event p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p \lor \Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absOrIntoEvent}) Absorption of $\lor$ into $\Event$}\\[\lgap]
  \> \>   $\Always p \lor p \lor \Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absAlwaysIntoOr}) Absorption of $\Always$ into $\lor$}\\[\lgap]
  \> \>   $ p \lor \Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absOrIntoEvent}) Absorption of $\lor$ into $\Event$}\\[\lgap]
  \> \>   $\Event p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

The absorption of $\Always$ corresponds to (\ref{E:IdemEvent}) the absorption of $\Event$,
and the exchange of $\Next$ and $\Always$ corresponds to (\ref{E:dNextEvent}) the exchange of $\Next$ and $\Event$.
\begin{equation}\label{E:IdemAlways}
\textbf{Absorption of $\Always$:}\quad \Always\Always p \equiv \Always p
\end{equation}

\emph{Proof}: (Kyle Sundman)
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$ with $p := \Always p$}\\[\lgap]
  \> \>   $\neg\Event\neg\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\neg\Event\Event\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:IdemEvent}) Absorption of $\Event$}\\[\lgap]
  \> \>   $\neg\Event\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $\Always p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:dNextAlways}
\textbf{Exchange of $\Next$ and $\Always$:}\quad \Next\Always p \equiv \Always\Next p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Next\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $\Next\neg\Event\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:selfDual}) Self-dual}\\[\lgap]
  \> \>   $\neg\Next\Event\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dNextEvent}) Exchange of $\Next$ and $\Event$ with $p := \neg p$}\\[\lgap]
  \> \>   $\neg\Event\Next\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:selfDual}) Self-dual}\\[\lgap]
  \> \>   $\neg\Event\neg\Next p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $\Always\Next p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

Theorem (\ref{E:impNext}) is unique to this system.
\begin{equation}\label{E:impNext}
p \impl \Always p \equiv p \impl \Next\Always p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p\impl \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$}\\[\lgap]
  \> \>   $p\impl p\land \Next\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(3.59) Implication $p\impl q \equivs \neg p \lor q$}\\[\lgap]
  \> \>   $\neg p\lor (p\land \Next\Always p)$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$}\\[\lgap]
  \> \>   $\neg p\lor (\neg\neg p\land \Next\Always p)$\\[\lgap]
  \> $=$  \>  \Hint{(3.44b) Absorption, $p \lor (\neg p \land q) \equiv p \lor q$ with $p,q := \neg p,\Next\Always p$}\\[\lgap]
  \> \>   $\neg p\lor \Next\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(3.59) Implication $p\impl q \equivs \neg p \lor q$}\\[\lgap]
  \> \>   $p \impl \Next\Always p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

The following four strengthening theorems for $\Always$ contrast with the weakening theorems
(\ref{E:impEvent}) and (\ref{E:nextEvent})
for $\Event$.
\begin{equation}\label{E:impAlways}
\textbf{Strengthening of $\Always$:}\quad \Always p \impl p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$}\\[\lgap]
  \> \>   $p \land \Next\Always p$\\[\lgap]
  \> $\impl$  \>  \Hint{(3.76b) Strengthening, $p\land q \impl p$}\\[\lgap]
  \> \>   $p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:impAlwaysE}
\textbf{Strengthening of $\Always$:}\quad \Always p \impl \Event p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:impAlways}) Strengthening of $\Always$}\\[\lgap]
  \> \>   $p$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:impEvent}) Weakening of $\Event$}\\[\lgap]
  \> \>   $\Event p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:impAlwaysN}
\textbf{Strengthening of $\Always$:}\quad \Always p \impl \Next p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$}\\[\lgap]
  \> \>   $p \land \Next\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dNextAlways}) Exchange of $\Next$ and $\Always$}\\[\lgap]
  \> \>   $p \land \Always\Next p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$ with $p := \Next p$}\\[\lgap]
  \> \>   $p \land \Next p \land \Next\Always\Next p$\\[\lgap]
  \> $\impl$  \>  \Hint{(3.76b) Strengthening, $p\land q \impl p$}\\[\lgap]
  \> \>   $\Next p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:impAlwaysNA}
\textbf{Strengthening of $\Always$:}\quad \Always p \impl \Next\Always p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$}\\[\lgap]
  \> \>   $p \land \Next\Always p$\\[\lgap]
  \> $\impl$  \>  \Hint{(3.76b) Strengthening, $p\land q \impl p$}\\[\lgap]
  \> \>   $\Next\Always p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

Theorem (\ref{E:exAlwaysNot}) states that if it is always the case that $p$ is false then it is not the case that $p$ is always true, but not the converse.
Suppose, for example, that $p$ continually oscillates between true and false over time.
Then, the consequent of (\ref{E:exAlwaysNot}) is true, but the antecedent is false.
Theorem (\ref{E:alwaysAndEvent}) shows how $\Event$ distributes over $\land$.
\begin{equation}\label{E:exAlwaysNot}
\textbf{Distributivity of $\neg$ over $\Always$:}\quad \Always\neg p \impl \neg\Always p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always\neg p$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:impAlwaysE}) Strengthening of $\Always$}\\[\lgap]
  \> \>   $\Event\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\neg\Always p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:alwaysAndEvent}
\textbf{Distributivity of $\Event$ over $\land$:}\quad \Always p \land \Event q \impl \Event (p \land q)
\end{equation}

\emph{Proof}: (Scott Staley)
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p \land \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $\Always p \land true \Until q$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:andUntilDist}) Distributivity of $\land$ over $\Until$ with $q,r :=true, q$}\\[\lgap]
  \> \>   $(p \land true) \Until (p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilAndEquiv}) Right distributivity of $\Until$ over $\land$}\\[\lgap]
  \> \>   $p\Until (p\land q) \land true \Until (p \land q)$\\[\lgap]
  \> $\impl$  \>  \Hint{(3.76b) Strengthening the antecedent $p\land q\impl p$}\\[\lgap]
  \> \>   $true \Until (p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
  \> \>   $\Event (p \land q)$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

Theorems (\ref{E:excludedMid}) and (\ref{E:excludedMidb}) are the linear temporal versions of the excluded middle axiom of propositional logic, (3.28) $p\lor\neg p$.
Theorems (\ref{E:contradiction}) and (\ref{E:contradictionb}) are the linear temporal versions of the contradiction theorem of propositional logic, (3.42) $p\land\neg p\equiv false$.
\begin{equation}\label{E:excludedMid}
\textbf{Temporal excluded middle:}\quad \Event p \lor \Always\neg p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event p \lor \Always\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
  \> \>   $\Event p \lor \neg\Event p$\\[\lgap]
  \> which is (3.28) Excluded middle, $p\lor\neg p$ with $p := \Event p$. \quad \myqed
\end{tabbing}
\begin{equation}\label{E:excludedMidb}
\textbf{Temporal excluded middle:}\quad \Always p \lor \Event\neg p
\end{equation}

\emph{Proof}: (Ray McIntyre)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p \lor \Event\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\Always p \lor \neg\Always p$\\[\lgap]
  \> which is (3.28) Excluded middle, $p\lor\neg p$ with $p := \Always p$. \quad \myqed
\end{tabbing}
\begin{equation}\label{E:contradiction}
\textbf{Temporal contradiction:}\quad \Event p \land \Always\neg p \equivs false
\end{equation}

\emph{Proof}: (Ray McIntyre)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event p \land \Always\neg p \equivs false$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
  \> \>   $\Event p \land \neg\Event p \equivs false$\\[\lgap]
  \> which is (3.42) Contradiction, $p\land\neg p \equivs false$ with $p := \Event p$. \quad \myqed
\end{tabbing}
\begin{equation}\label{E:contradictionb}
\textbf{Temporal contradiction:}\quad \Always p \land \Event\neg p \equivs false
\end{equation}

\emph{Proof}: (Ray McIntyre)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p \land \Event\neg p \equivs false$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\Always p \land \neg\Always p \equivs false$\\[\lgap]
  \> which is (3.42) Contradiction, $p\land\neg p \equivs false$ with $p := \Always p$. \quad \myqed
\end{tabbing}

Theorem (\ref{E:distAlwaysAnd}) shows that $\Always$, a universal operator, distributes over conjunction.
Because disjunction is existential, Theorem (\ref{E:distAlwaysOr}) shows that $\Always$ distributes over it in only one
direction.
Theorem (\ref{E:distAlwaysEquiv}) shows how $\Always$ distributes over $\equiv$.
Theorems  (\ref{E:eventImpAlways}) and (\ref{E:eventPImplEventQ}) show how $\Event$ distributes over $\impl$.
\begin{equation}\label{E:distAlwaysAnd}
\textbf{Distributivity of $\Always$ over $\land$:}\quad \Always (p \land q) \equiv \Always p \land \Always q
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$}\\[\lgap]
  \> \>   $\neg\Event\neg (p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.47a) De Morgan $\neg (p \land q) \equiv \neg p \lor \neg q$}\\[\lgap]
  \> \>   $\neg\Event (\neg p \lor \neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distEventOr}) Distributivity of $\Event$ over $\lor$}\\[\lgap]
  \> \>   $\neg (\Event\neg p \lor \Event\neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.47b) De Morgan, $\neg (p \lor q) \equiv \neg p \land \neg q$}\\[\lgap]
  \> \>   $\neg\Event\neg p \land \neg\Event\neg q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defAlways}) Definition of $\Always$, twice}\\[\lgap]
  \> \>   $\Always p \land \Always q$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:distAlwaysOr}
\textbf{Distributivity of $\Always$ over $\lor$:}\quad \Always p \lor \Always q \impl \Always (p \lor q)
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p \lor \Always q \impl \Always(p \lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.60) Implication, $p\impl q \equivs p\land q \equivs p$}\\[\lgap]
  \> \>   $(\Always p \lor \Always q) \land \Always(p \lor q) \equiv \Always p \lor \Always q$\\[\lgap]
  \> $=$  \>  \Hint{(3.46) Distributivity of $\land$ over $\lor$, $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$}\\[\lgap]
  \> \>   $(\Always (p \lor q) \land \Always p) \lor (\Always (p \lor q) \land \Always q) \equiv \Always p \lor \Always q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
  \> \>   $\Always(p \land (p \lor q)) \lor \Always(q \land (p \lor q)) \equiv \Always p \lor \Always q$\\[\lgap]
  \> $=$  \>  \Hint{(3.43a) Absorption, $p \land (p \lor q) \equiv p$ twice}\\[\lgap]
  \> \>   $\Always p \lor \Always q \equiv \Always p \lor \Always q$\\[\lgap]
  \> which is (3.5) Reflexivity of $\equiv$, $p\equiv p$ with $p:=\Always p \lor \Always q$. \quad \myqed
\end{tabbing}
\begin{equation}\label{E:distAlwaysEquiv}
\textbf{Distributivity of $\Always$ over $\equiv$:}\quad \Always (p \equiv q) \impl (\Always p \equiv \Always q)
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \equiv q) \impl (\Always p \equiv \Always q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.62) $p\impl (q\equiv r) \equivs p\land q\equivs p\land r$}\\[\lgap]
  \> \>   $\Always (p \equiv q) \land \Always p \equiv \Always (p \equiv q) \land \Always q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$, twice}\\[\lgap]
  \> \>   $\Always((p \equiv q) \land p) \equiv \Always((p \equiv q) \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.50) $p\land (q\equiv p)\equivs p\land q$ twice}\\[\lgap]
  \> \>   $\Always(p \land q) \equiv \Always (p \land q)$\\[\lgap]
  \> which is (3.5) Reflexivity of $\equiv$, $p\equiv p$ with $p:=\Always(p \land q)$. \quad \myqed
\end{tabbing}
\begin{equation}\label{E:eventImpAlways}
\textbf{Distributivity of $\Event$ over $\impl$:}\quad \Event (p \impl q) \equiv (\Always p \impl \Event q)
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event(p \impl q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.59) Implication, $p\impl q \equivs \neg p \lor q$}\\[\lgap]
  \> \>   $\Event(\neg p \lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distEventOr}) Distributivity of $\Event$ over $\lor$}\\[\lgap]
  \> \>   $\Event\neg p \lor \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\neg\Always p \lor \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(3.59) Implication, $p\impl q \equivs \neg p \lor q$}\\[\lgap]
  \> \>   $\Always p \impl \Event q$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:eventPImplEventQ}
\textbf{Distributivity of $\Event$ over $\impl$:}\quad (\Event p \impl \Event q) \impl \Event (p \impl q)
\end{equation}

\emph{Proof}: (Alexandra Angelo)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event (p \impl q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.59) Implication, $p\impl q \equivs \neg p \lor q$}\\[\lgap]
  \> \>   $\Event(\neg p \lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distEventOr}) Distributivity of $\Event$ over $\lor$}\\[\lgap]
  \> \>   $\Event\neg p \lor \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\neg \Always p \lor \Event q$\\[\lgap]
  \> $\foll$  \>  \Hint{(\ref{E:exAlwaysNot}) Distributivity of $\neg$ over $\Always$ and (4.2) Monotonicity of $\lor$}\\[\lgap]
  \> \>   $\Always \neg p \lor \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
  \> \>   $\neg\Event p \lor \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(3.59) Implication, $p\impl q \equivs \neg p \lor q$}\\[\lgap]
  \> \>   $\Event p \impl \Event q$ \quad \myqed
\end{tabbing}

The monotonicity theorems (\ref{E:alwaysImpNexts}), (\ref{E:alwaysImpEvents}), and (\ref{E:distAlwaysImp}) have $\Always (p \impl q)$
as the antecedent.
Theorem (\ref{E:distAlwaysImp}) can be considered distributivity of $\Always$ over $\impl$ as well.
Theorems (\ref{E:alwaysImpNexts}), (\ref{E:alwaysImpEvents}), and (\ref{E:distAlwaysImp}) show that all unary temporal
operators are monotonic.
\begin{equation}\label{E:alwaysImpNexts}
\textbf{Monotonicity of $\Next$:}\quad \Always (p \impl q) \impl (\Next p \impl \Next q)
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \impl q)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:impAlwaysN}) Strengthening of $\Always$}\\[\lgap]
  \> \>   $\Next (p \impl q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distNextImp}) Distributivity of $\Next$ over $\impl$}\\[\lgap]
  \> \>   $\Next p \impl \Next q$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:alwaysImpEvents}
\textbf{Monotonicity of $\Event$:}\quad \Always (p \impl q) \impl (\Event p \impl \Event q)
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \impl q) \impl (\Event p \impl \Event q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.59) Implication, $p\impl q \equivs \neg p \lor q$ three times}\\[\lgap]
  \> \>   $\neg\Always (\neg p \lor q) \lor \neg\Event p \lor \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\Event\neg (\neg p \lor q) \lor \neg\Event p \lor \Event q$\\[\lgap]  
  \> $=$  \>  \Hint{(3.47b) De Morgan, $\neg (p \lor q) \equiv \neg p \land \neg q$, and (3.12) Double negation, $\neg\neg p\equiv p$}\\[\lgap]
  \> \>   $\Event(p \land \neg q) \lor \neg\Event p \lor \Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distEventOr}) Distributivity of $\Event$ over $\lor$}\\[\lgap]
  \> \>   $\Event((p \land \neg q) \lor q) \lor \neg\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(3.44b) Absorption, $p \lor (\neg p \land q) \equiv p \lor q$}\\[\lgap]
  \> \>   $\Event(p \lor q) \lor \neg\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distEventOr}) Distributivity of $\Event$ over $\lor$}\\[\lgap]
  \> \>   $\Event p \lor \Event q \lor \neg\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(3.28) Excluded middle, $p\lor\neg p$ with $p := \Event p$}\\[\lgap]
  \> \>   $\Event q \lor true$\\[\lgap]
  \> $=$  \>  \Hint{(3.29) Zero of $\lor$, $p\lor true\equiv true$}\\[\lgap]
  \> \>   $true$\\[\lgap]
  \> which is (3.4). \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:distAlwaysImp}
\textbf{Monotonicity of $\Always$:}\quad \Always (p \impl q) \impl (\Always p \impl \Always q)
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \impl q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.60) Implication, $p\impl q \equivs p\land q \equivs p$}\\[\lgap]
  \> \>   $\Always (p \land q \equiv p)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:distAlwaysEquiv}) Distributivity of $\Always$ over $\equiv$}\\[\lgap]
  \> \>   $\Always(p \land q) \equiv \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
  \> \>   $\Always p \land \Always q \equiv \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(3.60) Implication, $p\impl q \equivs p\land q \equivs p$}\\[\lgap]
  \> \>   $\Always p \impl \Always q$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

\begin{figure}[t]
\centering
\begin{tabular}{ c c c }
  \begin{picture}(126,96)
  \thicklines
  \put(54,14) {\line(0,1){62}}
  \put(54,76) {\circle*{4}} \put(54,45) {\circle*{4}} \put(54,14) {\circle*{4}}
  \put(30,84) {$\Event p\land \Event q$}
  \put(58,60) {(\ref{E:distEventAnd})}
  \put(62,42) {$\Event (p\land q)$}
  \put(58,24) {(\ref{E:alwaysAndEvent})}
  \put(30,0) {$\Always p\land \Event q$}
  \end{picture}
&
  \begin{picture}(126,96)
  \thicklines
  \put(54,14) {\line(0,1){31}}
  \put(54,45) {\circle*{4}} \put(54,14) {\circle*{4}}
  \put(30,54) {$\Always (p\lor q)$}
  \put(58,24) {(\ref{E:distAlwaysOr})}
  \put(30,0) {$\Always p\lor \Always q$}
  \end{picture}
&
  \begin{picture}(126,96)
  \thicklines
  \put(54,14) {\line(0,1){31}}
  \put(54,45) {\circle*{4}} \put(54,14) {\circle*{4}}
  \put(30,54) {$\Always p\equiv \Always q$}
  \put(58,24) {(\ref{E:distAlwaysEquiv})}
  \put(30,0) {$\Always (p\equiv q)$}
  \end{picture}
\\
  \begin{picture}(126,116)
  \thicklines
  \put(54,14) {\line(0,1){31}}
  \put(54,45) {\circle*{4}} \put(54,14) {\circle*{4}}
  \put(38,54) {$\Always\Event p$}
  \put(58,24) {(\ref{E:eventAlwaysImp})}
  \put(38,0) {$\Event\Always p$}
  \end{picture}
&
  \begin{picture}(126,116)
  \thicklines
  \put(54,76) {\circle*{4}} \put(54,76) {\line(1,-1){31}}
  \put(23,45) {\circle*{4}} \put(23,45) {\line(1,1){31}} 
  \put(85,45) {\circle*{4}} \put(85,45) {\line(-1,-1){31}}
  \put(54,14) {\circle*{4}} \put(54,14) {\line(-1,1){31}}
  \put(48,84) {$\Event p$}
  \put(8,42) {$p$}
  \put(92,42) {$\Next p$}
  \put(48,0) {$\Always p$}
  \put(16,64) {(\ref{E:impEvent})}  \put(72,64) {(\ref{E:nextEvent})}
  \put(16,20) {(\ref{E:impAlways})} \put(72,20) {(\ref{E:impAlwaysN})}
  \end{picture}
&
  \begin{picture}(126,116)
  \thicklines
  \put(54,32) {\line(0,1){31}}
  \put(54,63) {\circle*{4}} \put(54,32) {\circle*{4}}
  \put(32,80){\fbox{\parbox{36pt}{\centering $\Event\neg p$ $\neg\Always p$}}}
  \put(32,8){\fbox{\parbox{36pt}{\centering $\Always\neg p$ $\neg\Event p$}}}
  \put(78,80) {(\ref{E:dualAlways})}
  \put(58,44) {(\ref{E:exAlwaysNot})}
  \put(78,8) {(\ref{E:dualEvent})}
  \end{picture}
\\
  \begin{picture}(126,128)
  \thicklines
  \put(109,76) {\circle*{4}} \put(109,76) {\line(1,-1){62}}
  \put(171,14) {\circle*{4}} \put(171,14) {\line(1,1){62}} \put(171,76) {\circle*{4}} \put(171,14) {\line(0,1){62}}
  \put(233,76) {\circle*{4}} \put(233,76) {\line(1,-1){62}} \put(295,14) {\circle*{4}}
  \put(78,82) {$\Next p\impl \Next q$} \put(144,82) {$\Always p\impl \Always q$}
  \put(200,94){\fbox{\parbox{56pt}{\centering $\Event(p\impl q)$ $\Always p \impl \Event q$}}}
  \put(144,0) {$\Always (p\impl q)$} \put(268,0) {$\Event p\impl \Event q$}
  \put(116,40) {(\ref{E:alwaysImpNexts})}
  \put(174,56) {(\ref{E:distAlwaysImp})}
  \put(208,40) {(\ref{E:alwaysImpEvents})}
  \put(272,40) {(\ref{E:eventPImplEventQ})}
  \put(266,94) {(\ref{E:eventImpAlways})}
  \end{picture}
\end{tabular}
\caption{Seven Hasse diagrams showing some implication relations of linear temporal logic.
\label{hasse}}
\end{figure}

Because the implication relation is reflexive, antisymmetric, and transitive, it defines a partially ordered set on linear temporal logic expressions.
Figure \ref{hasse} is a collection of seven Hasse diagrams showing some implication relations.
Each number in parentheses is a linear temporal logic theorem.
A number that labels an edge in a Hasse diagram is a implication theorem, and a number that labels a box is an equivalence theorem.
For example, edge (\ref{E:exAlwaysNot}) represents the theorem that $\Always\neg p$ implies $\neg\Always p$, and box (\ref{E:dualEvent}) represents the theorem that $\neg\Event p$ is equivalent to $\Always\neg p$.

The collection of theorems in this paper omit some implication theorems that are trivially derived by mutual transitivity.
For example, one such theorem is that $\Always\neg p$ implies $\Event \neg p$, which follows from the theorems that $\Always\neg p$ implies $\Event\neg p$ and that $\Event\neg p$ is equivalent to $\Event \neg p$.
The edge labeled by (\ref{E:exAlwaysNot}) thus represents four implication theorems, one for each combination of the two antecedents $\Always\neg p$ and $\neg\Event p$ and the two consequents $\Event\neg p$ and $\neg\Always p$.
Likewise, the edges labeled by (\ref{E:alwaysImpEvents}) and (\ref{E:eventPImplEventQ}) each represent two implication theorems.

\subsection{Proof metatheorems}

In the equational system $\mathcal{E}$, Gries and Schneider \cite{LADM} prove the metatheorem (9.16), which states that
$P$ is a theorem iff $(\all x\drrb P)$ is a theorem.
Theorems in $\mathcal{E}$ are thus said to be ``implicitly universally quantified.''
A similar concept applies to temporal logic theorems in $\mathcal{E}$ except that the implicit application is in the temporal dimension.
The following metatheorem shows that theorems ``implicitly always hold''.
Case 1 in the proof below is known as the temporal generalization rule \cite{Schn}, and Case 2 is known as the specialization rule \cite{Manna}.
\begin{equation}\label{E:metatheorem}
\textbf{Metatheorem:}\quad P \text{ is a theorem iff } \Always P \text{ is a theorem.}
\end{equation}

\emph{Proof}: The proof is by (4.7) Mutual implication.
The proof of each case is by (4.4) Deduction.

Case 1. If $P$ is a theorem then $\Always P$ is a theorem.\\
Suppose $P$ is a theorem.
Because all theorems are equivalent to each other, and (3.4) $true$ is a theorem, $P$ is equivalent to $true$.
Then, $\Always P$ can be proved to be a theorem as follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Always P$\\[\lgap]
\> $=$ \> \Hint{$P$ is a theorem} \\[\lgap]
\> \> $\Always true$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:alwaysTrue}) Truth of $\Always$} \\[\lgap]
\> \> $true$
\end{tabbing}

Case 2. If $\Always P$ is a theorem then $P$ is a theorem.\\
Suppose $\Always P$ is a theorem.
Then, $\Always P$ is equivalent to $true$.
$P$ can be proved to be a theorem by (4.7.1) Truth implication as follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $P$\\[\lgap]
\> $\foll$ \> \Hint{(\ref{E:impAlways}) Strengthening of $\Always$} \\[\lgap]
\> \> $\Always P$\\[\lgap]
\> $=$ \> \Hint{$\Always P$ is a theorem} \\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:metaEvent}
\textbf{Metatheorem $\Event$:}\quad \text{If } P\impl Q \text{ is a theorem then } \Event P\impl\Event Q \text{ is a theorem.}
\end{equation}

\emph{Proof}: The proof is by (4.4) Deduction.
Suppose $P\impl Q$ is a theorem.
Then, by (\ref{E:metatheorem}) Metatheorem, $\Always (P\impl Q)$ is a theorem.
Because all theorems are equivalent to each other, and (3.4) $true$ is a theorem, $\Always (P\impl Q)$ is equivalent to $true$.
Then, $\Event P\impl\Event Q$ can be proved to be a theorem by (4.7.1) Truth implication as follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Event P\impl\Event Q$\\[\lgap]
\> $\foll$ \> \Hint{(\ref{E:alwaysImpEvents}) Monotonicity of $\Event$} \\[\lgap]
\> \> $\Always (P\impl Q)$\\[\lgap]
\> $=$ \> \Hint{$\Always (P\impl Q)$ is a theorem} \\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:metaAlways}
\textbf{Metatheorem $\Always$:}\quad \text{If } P\impl Q \text{ is a theorem then } \Always P\impl\Always Q \text{ is a theorem.}
\end{equation}

\opt{doc}{
\emph{Proof}: The proof is by (4.4) Deduction.
Suppose $P\impl Q$ is a theorem.
Then, by (\ref{E:metatheorem}) Metatheorem, $\Always (P\impl Q)$ is a theorem.
Because all theorems are equivalent to each other, and (3.4) $true$ is a theorem, $\Always (P\impl Q)$ is equivalent to $true$.
Then, $\Always P\impl\Always Q$ can be proved to be a theorem by (4.7.1) Truth implication as follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Always P\impl\Always Q$\\[\lgap]
\> $\foll$ \> \Hint{(\ref{E:distAlwaysImp}) Monotonicity of $\Always$} \\[\lgap]
\> \> $\Always (P\impl Q)$\\[\lgap]
\> $=$ \> \Hint{$\Always (P\impl Q)$ is a theorem} \\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}
}
\opt{student}{
\emph{Proof}:\\
Exercise for the student.\\
}

\subsection{Always, continued}\label{section-always-continued}

The next group of four distributivity theorems show how $\Always\Event$ and $\Event\Always$
distribute over conjunction and disjunction.
Theorem (\ref{E:distAlwaysEventAnd}) shows that $\Always\Event$ distributes over conjunction only in one direction.
Similarly, Theorem (\ref{E:distEventAlwaysOr}) shows that $\Event\Always$ distributes over disjunction only in one direction.
However, Theorems (\ref{E:distAlwaysEventOr}) and (\ref{E:distEventAlwaysAnd}) show that $\Always\Event$ distributes over
disjunction and $\Event\Always$ distributes over conjunction in both directions.
\begin{equation}\label{E:distAlwaysEventAnd}
\textbf{Distributivity of $\Always\Event$ over $\land$:}\quad \Always\Event(p \land q) \impl \Always\Event p \land \Always\Event q
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always\Event(p \land q)$\\[\lgap]
  \> $\impl$  \>  \Hint{Lemma: $\Always\Event(p \land q) \impl \Always(\Event p \land \Event q)$}\\[\lgap]
  \> \>   $\Always(\Event p \land \Event q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
  \> \>   $\Always\Event p \land \Always\Event q$
\end{tabbing}

\emph{Proof of Lemma}:
By (\ref{E:metaAlways}) Metatheorem $\Always$ and (\ref{E:distEventAnd}) Distributivity of $\Event$ over $\land$ the following is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always\Event(p \land q) \impl \Always(\Event p \land \Event q)$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:distEventAlwaysOr}
\textbf{Distributivity of $\Event\Always$ over $\lor$:}\quad \Event\Always p \lor \Event\Always q \impl \Event\Always (p \lor q)
\end{equation}

\emph{Proof}: (Scott Staley)\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event\Always p \lor \Event\Always q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distEventOr}) Distributivity of $\Event$ over $\lor$}\\[\lgap]
  \> \>   $\Event(\Always p \lor \Always q)$\\[\lgap]
  \> $\impl$  \>  \Hint{Lemma: $\Event(\Always p \lor \Always q) \impl \Event\Always (p \lor q)$}\\[\lgap]
  \> \>   $\Event\Always (p \lor q)$
\end{tabbing}

\emph{Proof of Lemma}:
By (\ref{E:metaEvent}) Metatheorem $\Event$ and (\ref{E:distAlwaysOr}) Distributivity of $\Always$ over $\lor$ the following is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event(\Always p \lor \Always q) \impl \Event\Always (p \lor q)$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}
\begin{equation}\label{E:distAlwaysEventOr}
\textbf{Distributivity of $\Always\Event$ over $\lor$:}\quad \Always\Event(p \lor q) \equiv \Always\Event p \lor \Always\Event q
\end{equation}

\emph{Proof}: The proof is by (4.7) Mutual implication.
The proof in the first direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always\Event p \lor \Always\Event q$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:distAlwaysOr}) Distributivity of $\Always$ over $\lor$}\\[\lgap]
  \> \>   $\Always(\Event p \lor \Event q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distEventOr}) Distributivity of $\Event$ over $\lor$}\\[\lgap]
  \> \>   $\Always\Event(p \lor q)$
\end{tabbing}
The proof in the second direction is by (4.7.1) Truth implication.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $true$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:alwaysAndEvent}) with $p,q:=\Event(p\lor q),\Always\neg p$}\\[\lgap]
  \> \>   $\Always \Event(p\lor q) \land \Event \Always\neg p \impl \Event (\Event(p\lor q) \land \Always\neg p)$\\[\lgap]
  \> $\impl$  \>  \Hint{Lemma: $\Event (\Event(p\lor q) \land \Always\neg p)\impl\Event q$}\\[\lgap]
  \> \>   $\Always \Event(p\lor q) \land \Event \Always\neg p \impl \Event q$
\end{tabbing}
Now, by (\ref{E:metaAlways}) Metatheorem $\Always$, the following is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (\Always \Event(p\lor q) \land \Event \Always\neg p) \impl \Always\Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
  \> \>   $\Always\Always \Event(p\lor q) \land \Always\Event \Always\neg p \impl \Always\Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:IdemAlways}) Absorption of $\Always$}\\[\lgap]
  \> \>   $\Always \Event(p\lor q) \land \Always\Event \Always\neg p \impl \Always\Event q$\\[\lgap]
  \> $\impl$  \>  \Hintfirst{(\ref{E:eventAlwaysImp}) $\Event \Always$ implication and (3.76.2) $(p\impl q) \impl ((q\impl r)\impl (p\impl r))$}\\[\lgap]
  \> \>  \Hintlast{and (4.3) Monotonicity of $\land$}\\[\lgap]
  \> \>   $\Always \Event(p\lor q) \land \Event\Always \Always\neg p \impl \Always\Event q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:IdemAlways}) Absorption of $\Always$}\\[\lgap]
  \> \>   $\Always \Event(p\lor q) \land \Event\Always \neg p \impl \Always\Event q$\\[\lgap]
  \> $=$  \>  \Hint{(3.65) Shunting, $p\land q\impl r\equivs p\impl (q\impl r)$}\\[\lgap]
  \> \>   $\Always \Event(p\lor q) \impl (\Event\Always \neg p \impl \Always\Event q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualEvent}) Dual of $\Event$ and (\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\Always \Event(p\lor q) \impl (\neg\Always\Event p \impl \Always\Event q)$\\[\lgap]
	\> $=$  \>  \Hint{(3.59) Implication $p\impl q \equivs \neg p \lor q$}\\[\lgap]
  \> \>   $\Always \Event(p\lor q) \impl \Always\Event p \lor \Always\Event q$
\end{tabbing}

\emph{Proof of Lemma}:
The proof is by (4.7.1) Truth implication.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $true$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:alwaysAndEvent}) with $p,q:=\neg p, p\lor q$}\\[\lgap]
  \> \>   $\Always \neg p \land \Event (p\lor q) \impl \Event (\neg p \land (p\lor q))$\\[\lgap]
  \> $=$ \> \Hint{(3.44a) Absorption, $p\land (\neg p\lor q)\equiv p\land q$} \\[\lgap]
  \> \>   $\Always \neg p \land \Event (p\lor q) \impl \Event (\neg p \land q)$
\end{tabbing}
Now, by (\ref{E:metaEvent}) Metatheorem $\Event$, the following is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event(\Always \neg p \land \Event (p\lor q)) \impl \Event\Event (\neg p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:IdemEvent}) Absorption of $\Event$}\\[\lgap]
  \> \>   $\Event(\Always \neg p \land \Event (p\lor q)) \impl \Event (\neg p \land q)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:distEventAnd}) Distributivity of $\Event$ over $\land$}\\[\lgap]
  \> \>   $\Event(\Always \neg p \land \Event (p\lor q)) \impl \Event \neg p \land \Event q$\\[\lgap]
  \> $\impl$  \> \Hint{(3.76b) Strengthening, $p\land q \impl p$} \\[\lgap]
  \> \>   $\Event(\Always \neg p \land \Event (p\lor q)) \impl \Event q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:distEventAlwaysAnd}
\textbf{Distributivity of $\Event\Always$ over $\land$:}\quad \Event\Always(p \land q) \equiv \Event\Always p \land \Event\Always q
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event\Always (p\land q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$}\\[\lgap]
  \> \>   $\Event\Always (\neg\neg p\land \neg\neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.47b) De Morgan, $\neg (p \lor q) \equiv \neg p \land \neg q$}\\[\lgap]
  \> \>   $\Event\Always \neg(\neg p\lor \neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualEvent}) Dual of $\Event$ and (\ref{E:dualAlways}) Dual of $\Always$}\\[\lgap]
  \> \>   $\neg\Always\Event (\neg p\lor \neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distAlwaysEventOr}) Distributivity of $\Always\Event$ over $\lor$}\\[\lgap]
  \> \>   $\neg(\Always\Event \neg p\lor \Always\Event \neg q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$ and (\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
  \> \>   $\neg(\neg \Event\Always p\lor  \neg \Event\Always q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.47a) De Morgan $\neg (p \land q) \equiv \neg p \lor \neg q$}\\[\lgap]
  \> \>   $\neg\neg (\Event\Always p\land \Event\Always q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$}\\[\lgap]
  \> \>   $\Event\Always p\land \Event\Always q$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

The absorption theorems, (\ref{E:absEvent}) and (\ref{E:absAlways}), together with absorption theorems
(\ref{E:IdemEvent}) and (\ref{E:IdemAlways}), allow any arbitrary string of $\Event$ and $\Always$ operators
of any arbitrary length to be collapsed into one of four expressions: \;$\Event p$, \;$\Always p$,
\;$\Always\Event p$, or \;$\Event\Always p$.
\begin{equation}\label{E:absEvent}
\textbf{Absorption of $\Event$ into $\Always\Event$:}\quad \Event\Always\Event p \equiv \Always\Event p
\end{equation}

\emph{Proof}: The proof is by (4.7) Mutual implication.
The proof in the first direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Event\Always\Event p$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:eventAlwaysImp}) $\Event\Always$ implication}\\[\lgap]
  \> \>   $\Always\Event\Event p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:IdemEvent}) Absorption of $\Event$}\\[\lgap]
  \> \>   $\Always\Event p$
\end{tabbing}
The proof in the second direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always\Event p$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:impEvent}) Weakening of $\Event$}\\[\lgap]
  \> \>   $\Event\Always\Event p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:absAlways}
\textbf{Absorption of $\Always$ into $\Event\Always$:}\quad \Always\Event\Always p \equiv \Event\Always p
\end{equation}

\emph{Proof}:
\opt{doc}{
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always\Event\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$}\\[\lgap]
  \> \>   $\Always\Event\Always \neg\neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$ and (\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
  \> \>   $\neg\Event\Always\Event \neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absEvent}) Absorption of $\Event$ into $\Always\Event$}\\[\lgap]
  \> \>   $\neg\Always\Event \neg p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualAlways}) Dual of $\Always$ and (\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
  \> \>   $\neg\neg\Event\Always p$\\[\lgap]
  \> $=$  \>  \Hint{(3.12) Double negation, $\neg\neg p\equiv p$}\\[\lgap]
  \> \>   $\Event\Always p$ \quad \myqed
\end{tabbing}
}
\opt{student}{
Exercise for the student.\\
}

The metatheorems and absorption laws imply the following intuitive theorem.
If $p$ will eventually be always true, and it is always the case that $q$ will be eventually true, then it is always the case that $p\land q$ will eventually be true.
\begin{equation}\label{E:eventAlwaysPAndAlwaysEventQ}
\Event\Always p\land \Always\Event q \impl \Always\Event (p\land q)
\end{equation}

\emph{Proof}: (Scott Staley) By (\ref{E:alwaysAndEvent}) and (\ref{E:metaAlways}) Metatheorem $\Always$, the following is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \>   $\Always (\Always p \land \Event q) \impl \Always\Event (p \land q)$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
\> \>   $\Always \Always p \land \Always\Event q \impl \Always\Event (p \land q)$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:IdemAlways}) Absorption of $\Always$}\\[\lgap]
\> \>   $\Always p \land \Always\Event q \impl \Always\Event (p \land q)$\\[\lgap]
\> $=$  \>  \Hint{(3.65) Shunting, $p\land q\impl r\equivs p\impl (q\impl r)$}\\[\lgap]
\> \>   $\Always p \impl (\Always\Event q \impl \Always\Event (p \land q))$
\end{tabbing}
Now, by (\ref{E:metaEvent}) Metatheorem $\Event$, the following is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \>   $\Event\Always p \impl \Event(\Always\Event q \impl \Always\Event (p \land q))$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:eventImpAlways}) Distributivity of $\Event$ over $\impl$}\\[\lgap]
\> \>   $\Event\Always p \impl (\Always\Always\Event q \impl \Event\Always\Event (p \land q))$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:IdemAlways}) Absorption of $\Always$ and (\ref{E:absEvent}) Absorption of $\Event$ into $\Always$}\\[\lgap]
\> \>   $\Event\Always p \impl (\Always\Event q \impl \Always\Event (p \land q))$\\[\lgap]
\> $=$  \>  \Hint{(3.65) Shunting, $p\land q\impl r\equivs p\impl (q\impl r)$}\\[\lgap]
\> \>   $\Event\Always p\land \Always\Event q \impl \Always\Event (p\land q)$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:PrProofRule}
\textbf{Progress proof rule:}\quad \Event\Always p \land \Always(\Always p \impl \Event q) \impl \Event q
\end{equation}

\emph{Proof}: (Scott Staley)\quad By (3.77) Modus ponens, $p\land (p\impl q)\impl q$ with $p,q:=\Always p,\Event q$, the following is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \>   $\Always p\land (\Always p\impl \Event q)\impl \Event q$\\[\lgap]
\> $=$  \>  \Hint{(3.65) Shunting $p\land q\impl r\equivs p\impl (q\impl r)$}\\[\lgap]
\> \>   $\Always p\impl ((\Always p\impl \Event q)\impl \Event q$)
\end{tabbing}
Now, by (\ref{E:metaEvent}) Metatheorem $\Event$, the following is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \>   $\Event\Always p\impl \Event((\Always p\impl \Event q)\impl \Event q$)\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:eventImpAlways}) Distributivity of $\Event$ over $\impl$}\\[\lgap]
\> \>   $\Event\Always p\impl (\Always(\Always p\impl \Event q)\impl \Event\Event q$)\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:IdemEvent}) Absorption of $\Event$}\\[\lgap]
\> \>   $\Event\Always p\impl (\Always(\Always p\impl \Event q)\impl \Event q$)\\[\lgap]
\> $=$  \>  \Hint{(3.65) Shunting, $p\land q\impl r\equivs p\impl (q\impl r)$}\\[\lgap]
\> \>   $\Event\Always p \land \Always(\Always p \impl \Event q) \impl \Event q$ \quad \myqed
\end{tabbing}

\subsection{Wait}\label{section-wait}

$p\Until q$ requires $p$ to be true until $q$, which is guaranteed to eventually be true.
$p\Wait q$ has no such guarantee.
That is, if $q$ is eventually true then $p$ is true until that time.
But, if $q$ is not eventually true then $p$ must be true always.
Equations (\ref{E:defWait}) and (\ref{E:notWait}) are the only defining axioms for the \textit{wait} operator.
(Note that Schneider \cite{Schn} uses the symbol $\Until$ for the \textit{wait} operator and calls it ``unless''.)
\begin{equation}\label{E:defWait}
\textbf{Definition of $\Wait$:}\quad p \Wait q \equiv \Always p \lor p \Until q 
\end{equation}
\begin{equation}\label{E:notWait}
\textbf{Axiom, Distributivity of $\neg$ over $\Wait$:}\quad \neg (p \Wait q) \equiv \neg q \Until (\neg p \land \neg q)
\end{equation}

The defining equation gives $\Wait$ in terms of $\Until$. The following theorem gives $\Until$ in terms of $\Wait$.
\begin{equation}\label{E:untilFromWait}
\textbf{$\Until$ in terms of $\Wait$:}\quad p \Until q \equiv p \Wait q\land \Event q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Until q \equiv p \Wait q\land \Event q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p \Until q \equiv (\Always p\lor p \Until q)\land \Event q$\\[\lgap]
\> $=$ \> \Hint{(3.46) Distributivity of $\land$ over $\lor$, $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$} \\[\lgap]
\> \> $p \Until q \equiv (\Always p\land \Event q)\lor (p \Until q\land \Event q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:absEventIntoUntil}) Absorption of $\Event$ into $\Until$} \\[\lgap]
\> \> $p \Until q \equiv (\Always p\land \Event q)\lor p \Until q$\\[\lgap]
\> $=$ \> \Hint{(3.57) Definition of implication, $p\impl q\equivs p\lor q \equivs q$} \\[\lgap]
\> \> $\Always p\land \Event q\impl p\Until q$\\[\lgap]
\> which is (\ref{E:axiomUntilImpl}) $\Until$ implication. \quad \myqed
\end{tabbing}

(\ref{E:notUntil}) proves Distributivity of $\neg$ over $\Until$ using (\ref{E:notWait}) Axiom, Distributivity of $\neg$ over $\Wait$.
Apparently, the reverse is not possible.
That is, if (\ref{E:notUntil}) is taken as the axiom instead of (\ref{E:notWait}), it is apparently impossible to prove (\ref{E:notWait}).
\begin{equation}\label{E:notUntil}
\textbf{Distributivity of $\neg$ over $\Until$:}\quad \neg (p \Until q) \equiv \neg q \Wait (\neg p \land \neg q)
\end{equation}

\emph{Proof}: (Michael Ortiz)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\neg q \Wait (\neg p \land \neg q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always\neg q \lor \neg q\Until (\neg p \land \neg q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:notWait}) Distributivity of $\neg$ over $\Wait$} \\[\lgap]
\> \> $\Always\neg q \lor \neg (p \Wait q)$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
\> \> $\neg (p \Wait q) \lor \neg\Event q $\\[\lgap]
\> $=$  \>  \Hint{(3.47a) De Morgan $\neg (p \land q) \equiv \neg p \lor \neg q$}\\[\lgap]
\> \> $\neg (p \Wait q \land \Event q)$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:untilFromWait}) $\Until$ in terms of $\Wait$}\\[\lgap]
\> \> $\neg (p \Until q)$ \quad \myqed
\end{tabbing}

(\ref{E:untilImplWait}) shows that $p\Until q$ is stronger than $p\Wait q$.
Therefore, by contrapositive, $\neg (p \Wait q)$ is stronger than $\neg (p \Until q)$.
\begin{equation}\label{E:untilImplWait}
p\Until q\impl p\Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilFromWait})} \\[\lgap]
\> \> $p \Wait q\land \Event q$\\[\lgap]
\> $\impl$ \> \Hint{(3.76b) Strengthening, $p\land q \impl p$} \\[\lgap]
\> \> $p \Wait q$ \quad \myqed
\end{tabbing}

Distributivity of $\land$ over $\Wait$ corresponds to, and is derived from, (\ref{E:andUntilDist}) Distributivity of $\land$ over $\Until$.
\begin{equation}\label{E:andWaitDist}
\textbf{Distributivity of $\land$ over $\Wait$:}\quad \Always p \land q \Wait r \impl (p \land q) \Wait (p \land r)
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always p \land q \Wait r$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
  \> \>   $\Always p \land (\Always q \lor q\Until r)$\\[\lgap]
  \> $=$  \>  \Hint{(3.46) Distributivity of $\land$ over $\lor$, $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$}\\[\lgap]
  \> \>   $(\Always p \land \Always q) \lor (\Always p\land q\Until r)$\\[\lgap]
  \> $\impl$  \>  \Hintfirst{(\ref{E:andUntilDist}) Distributivity of $\land$ over $\Until$ and (4.2) Monotonicity of $\lor$,}\\[\lgap]
  \> \>  \Hintlast{$(p\impl q) \impl (p\lor r \impl q\lor r)$}\\[\lgap]
  \> \>   $(\Always p \land \Always q) \lor (p\land q)\Until (p\land r)$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$} \\[\lgap]
  \> \>   $\Always (p \land q) \lor (p\land q)\Until (p\land r)$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
  \> \>   $(p \land q) \Wait (p \land r)$ \quad \myqed
\end{tabbing}

Perpetuity for the \textit{wait} operator corresponds to (\ref{E:eventuality}) Eventuality
for the \textit{until} operator.
The \textit{always} operator, which is universal, is in the antecedent of the implication in Perpetuity, while
the \textit{eventually} operator, which is existential, is in the consequent of the implication in Eventuality.
\begin{equation}\label{E:alwaysImpWait}
\textbf{Perpetuity:}\quad \Always p \impl p \Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Always p$\\[\lgap]
\> $\impl$ \> \Hint{(3.76a) Weakening, $p\impl p\lor q$} \\[\lgap]
\> \> $\Always p \lor p \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p \Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitNextDist}
\textbf{Distributivity of $\Next$ over $\Wait$:}\quad \Next (p \Wait q) \equiv \Next p \Wait \Next q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Next (p \Wait q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Next(\Always p\lor p\Until q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:distNextOr}) Distributivity of $\Next$ over $\lor$} \\[\lgap]
\> \> $\Next \Always p\lor \Next(p\Until q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:dNextAlways}) Exchange of $\Next$ and $\Always$ and (\ref{E:distNextUntil}) Distributivity of $\Next$ over $\Until$} \\[\lgap]
\> \> $\Always \Next p\lor \Next p\Until \Next q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) with $p,q := \Next p, \Next q$} \\[\lgap]
\> \> $\Next p \Wait \Next q$ \quad \myqed
\end{tabbing}

Expansion of the \textit{wait} operator (\ref{E:expansionWait}) corresponds to expansion of the \textit{until} operator (\ref{E:expansionUntil}).
\begin{equation}\label{E:expansionWait}
\textbf{Expansion of $\Wait$:}\quad p \Wait q \equiv q \lor (p \land \Next (p \Wait q))
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $q \lor (p \land \Next (p \Wait q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $q \lor (p \land \Next (\Always p\lor p \Until q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:distNextOr}) Distributivity of $\Next$ over $\lor$} \\[\lgap]
\> \> $q \lor (p \land (\Next\Always p\lor \Next (p \Until q)))$\\[\lgap]
\> $=$ \> \Hint{(3.46) Distributivity of $\land$ over $\lor$, $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$}\\[\lgap]
\> \> $q \lor (p \land \Next\Always p)\lor (p \land \Next(p \Until q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionAlways}) Expansion of $\Always$}\\[\lgap]
\> \> $q \lor \Always p\lor (p \land \Next(p \Until q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionUntil}) Expansion of $\Until$}\\[\lgap]
\> \> $\Always p\lor p \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p \Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitExcludedMiddle}
\Wait \textbf{excluded middle:}\quad p \Wait q \lor p\Wait \neg q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait q \lor p\Wait \neg q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion, twice} \\[\lgap]
\> \> $q\lor (p\land \Next (p\Wait q))\lor \neg q \lor (p\land \Next (p\Wait \neg q))$\\[\lgap]
\> $=$ \> \Hint{(3.28) Excluded middle, $p\lor \neg p$} \\[\lgap]
\> \> $true \lor (p\land \Next (p\Wait q)) \lor (p\land \Next (p\Wait \neg q))$\\[\lgap]
\> $=$ \> \Hint{(3.29) Zero of $\lor$, $p\lor true\equiv true$} \\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}

Left zero of \textit{wait} corresponds to (\ref{E:untilFalse}) Right zero of \textit{until}.
\begin{equation}\label{E:leftZeroWait}
\textbf{Left zero of $\Wait$:}\quad true \Wait q \equiv true
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $true \Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always true \lor true\Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:alwaysTrue}) Truth of $\Always$} \\[\lgap]
\> \> $true \lor true\Until q$\\[\lgap]
\> $=$ \> \Hint{(3.29) Zero of $\lor$, $p\lor true \equiv true$}\\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}

The next four distributive theorems for the \textit{wait} operator correspond to, and are proved from,
the distributive axioms for the \textit{until} operator
(\ref{E:untilOrEquiv}), (\ref{E:untilOrImp}), (\ref{E:untilAndImp}), and (\ref{E:untilAndEquiv}).
\begin{equation}\label{E:waitOrDist}
\textbf{Left distributivity of $\Wait$ over $\lor$:}\quad p \Wait (q \lor r) \equiv p \Wait q \lor p \Wait r
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait q \lor p \Wait r$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$, twice} \\[\lgap]
\> \> $\Always p\lor p \Until q \lor \Always p\lor p \Until r$\\[\lgap]
\> $=$ \> \Hint{(3.26) Idempotency of $\lor$, $p \lor p \equiv p$} \\[\lgap]
\> \> $\Always p\lor p \Until q \lor p \Until r$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilOrEquiv}) Left Distributivity of $\Until$ over $\lor$} \\[\lgap]
\> \> $\Always p\lor p \Until (q \lor r)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p \Wait (q \lor r)$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:rightWaitOrDist}
\textbf{Right distributivity of $\Wait$ over $\lor$:}\quad p \Wait r \lor q \Wait r \impl (p \lor q) \Wait r
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait r \lor q \Wait r$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p \lor \Always q\lor p \Until r \lor q \Until r$\\[\lgap]
\> $\impl$ \> \Hintfirst{(\ref{E:distAlwaysOr}) Distributivity of $\Always$ over $\lor$ and (4.2) Monotonicity of $\lor$,} \\[\lgap]
\>  \> \Hintlast{$(p\impl q)\impl (p\lor r \impl q\lor r)$} \\[\lgap]
\> \> $\Always (p \lor q)\lor p \Until r \lor q \Until r$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:untilOrImp}) Right distributivity of $\Until$ over $\lor$ and (4.2) Monotonicity of $\lor$} \\[\lgap]
\> \> $\Always (p \lor q)\lor (p \lor q) \Until r$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $(p \lor q) \Wait r$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:leftWaitAndDist}
\textbf{Left distributivity of $\Wait$ over $\land$:}\quad p \Wait (q \land r) \impl p \Wait q \land p \Wait r
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait (q \land r)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p\lor p \Until (q \land r)$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:untilAndImp}) Left Distributivity of $\Until$ over $\land$ and (4.2) Monotonicity of $\lor$} \\[\lgap]
\> \> $\Always p\lor (p \Until q \land p \Until r)$\\[\lgap]
\> $=$ \> \Hint{(3.45) Distributivity of $\lor$ over $\land$, $p\lor (q\land r) \equiv (p\lor q) \land (p\lor r)$} \\[\lgap]
\> \> $(\Always p\lor p \Until q) \land (\Always p\lor p \Until r)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$, twice} \\[\lgap]
\> \> $p \Wait q \land p \Wait r$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:rightWaitAndDist}
\textbf{Right distributivity of $\Wait$ over $\land$}\quad (p \land q) \Wait r\equiv p \Wait r \land q \Wait r
\end{equation}

\emph{Proof}: The proof is by (4.7) Mutual implication.
The proof in the first direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Wait r \land q \Wait r$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
  \> \>   $(\Always p\lor p \Until r) \land (\Always q\lor q \Until r)$\\[\lgap]
  \> $=$ \> \Hint{(3.46) Distributivity of $\land$ over $\lor$, $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r) \lor (\Always p \land q\Until r) \lor (\Always q\land p \Until r)$\\[\lgap]
  \> $\foll$ \> \Hint{(3.76a) Weakening, $p\impl p\lor q$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r)$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:untilAndEquiv}) Right distributivity of $\Until$ over $\land$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p\land q) \Until r$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
  \> \>   $\Always (p\land q) \lor (p\land q) \Until r$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
  \> \>   $(p\land q) \Wait r$
\end{tabbing}
The proof in the second direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Wait r \land q \Wait r$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
  \> \>   $(\Always p\lor p \Until r) \land (\Always q\lor q \Until r)$\\[\lgap]
  \> $=$ \> \Hint{(3.46) Distributivity of $\land$ over $\lor$, $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r) \lor (\Always p \land q\Until r) \lor (\Always q\land p \Until r)$\\[\lgap]
  \> $\impl$ \> \Hint{(\ref{E:andUntilDist}) Distributivity of $\land$ over $\Until$, twice and (4.2) Monotonicity of $\lor$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r) \lor (p \land q) \Until (p \land r) \lor (p \land q) \Until (q \land r)$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:untilOrEquiv}) Left distributivity of $\Until$ over $\lor$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r) \lor (p \land q) \Until ((p \land r) \lor (q \land r))$\\[\lgap]
  \> $=$ \> \Hint{(3.46) Distributivity of $\land$ over $\lor$, $p\land (q\lor r)\equiv (p\land q)\lor (p\land r)$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r) \lor (p \land q) \Until (r \land (p \lor q))$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:untilAndEquiv}) Right distributivity of $\Until$ over $\land$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r) \lor (p \Until (r \land (p \lor q)) \land q \Until (r \land (p \lor q)))$\\[\lgap]
  \> $\impl$ \> \Hint{(\ref{E:untilAndImp}) Left distributivity of $\Until$ over $\land$, twice and (4.2) Monotonicity of $\lor$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r) \lor (p \Until r \land p \Until (p \lor q) \land q \Until r \land q \Until (p \lor q))$\\[\lgap]
  \> $\impl$ \> \Hint{(3.76b) Strengthening, $p \land q \impl p$ and (4.2) Monotonicity of $\lor$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r) \lor (p \Until r\land q\Until r)$\\[\lgap]
  \> $=$ \> \Hint{(3.26) Idempotency of $\lor$, $p\lor p \equiv p$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \Until r\land q\Until r)$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:untilAndEquiv}) Right distributivity of $\Until$ over $\land$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \land q) \Until r$\\[\lgap]
  \> $\impl$ \> \Hint{(\ref{E:untilImplWait}) and (4.2) Monotonicity of $\lor$} \\[\lgap]
  \> \>   $(\Always p\land \Always q) \lor (p \land q) \Wait r$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$} \\[\lgap]
  \> \>   $\Always (p \land q) \lor (p \land q) \Wait r$\\[\lgap]
  \> $\impl$ \> \Hint{(\ref{E:alwaysImpWait}) Perpetuity and  (4.2) Monotonicity of $\lor$} \\[\lgap]
  \> \>   $((p \land q) \Wait r) \lor (p \land q) \Wait r$\\[\lgap]
  \> $=$ \> \Hint{(3.26) Idempotency of $\lor$, $p\lor p \equiv p$} \\[\lgap]
  \> \>   $(p \land q) \Wait r$ \quad \myqed
\end{tabbing}

Both $\Wait$ and $\Until$ obey the following disjunction and conjunction rules, which give rise, in turn, to expanded distributivity theorems of $\neg$ over $\Wait$ and $\Until$.
\begin{equation}\label{E:disRuleWait}
\textbf{Disjunction rule of $\Wait$:}\quad p\Wait q\equiv (p\lor q)\Wait q
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\Wait q$\\[\lgap]
\> $=$ \> \Hint{(3.12) Double negation, $\neg\neg p\equiv p$} \\[\lgap]
\> \> $\neg\neg (p\Wait q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:notWait}) Distributivity of $\neg$ over $\Wait$} \\[\lgap]
\> \> $\neg (\neg q\Until (\neg p\land \neg q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:notUntil}) Distributivity of $\neg$ over $\Until$} \\[\lgap]
\> \> $\neg (\neg p\land \neg q)\Wait (q\land \neg (\neg p\land \neg q))$\\[\lgap]
\> $=$ \> \Hint{(3.47a) De Morgan, $\neg (p\land q)\equiv \neg p\lor \neg q$, twice} \\[\lgap]
\> \> $( p\lor q)\Wait (q\land (p\lor q))$\\[\lgap]
\> $=$ \> \Hint{(3.43a) Absorption, $p\land (p\lor q) \equiv p$} \\[\lgap]
\> \> $(p\lor q) \Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:disRuleUntil}
\textbf{Disjunction rule of $\Until$:}\quad p\Until q\equiv (p\lor q)\Until q
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\Until q$\\[\lgap]
\> $=$ \> \Hint{(3.12) Double negation, $\neg\neg p\equiv p$} \\[\lgap]
\> \> $\neg\neg (p\Until q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:notUntil}) Distributivity of $\neg$ over $\Until$} \\[\lgap]
\> \> $\neg (\neg q\Wait (\neg p\land \neg q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:notWait}) Distributivity of $\neg$ over $\Wait$} \\[\lgap]
\> \> $\neg (\neg p\land \neg q)\Until (q\land \neg (\neg p\land \neg q))$\\[\lgap]
\> $=$ \> \Hint{(3.47a) De Morgan, $\neg (p\land q)\equiv \neg p\lor \neg q$, twice} \\[\lgap]
\> \> $( p\lor q)\Until (q\land (p\lor q))$\\[\lgap]
\> $=$ \> \Hint{(3.43a) Absorption, $p\land (p\lor q) \equiv p$} \\[\lgap]
\> \> $(p\lor q) \Until q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:ruleWait}
\textbf{Rule of $\Wait$:}\quad \neg q \Wait q
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\neg q\Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:disRuleWait}) Disjunction rule of $\Wait$} \\[\lgap]
\> \> $(\neg q\lor q)\Wait q$\\[\lgap]
\> $=$ \> \Hint{(3.28) Excluded middle $p\lor \neg p$} \\[\lgap]
\> \> $true\Wait q$\\[\lgap]
\> $=$ \> \Hint{\ref{E:leftZeroWait}) Left zero of $\Wait$} \\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:ruleUntil}
\textbf{Rule of $\Until$:}\quad \neg q \Until q\equivs \Event q
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\neg q\Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:disRuleUntil}) Disjunction rule of $\Until$} \\[\lgap]
\> \> $(\neg q\lor q)\Until q$\\[\lgap]
\> $=$ \> \Hint{(3.28) Excluded middle $p\lor \neg p$} \\[\lgap]
\> \> $true\Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defEvent}) Definition of $\Until$} \\[\lgap]
\> \> $\Event q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:pImplQWaitP}
(p\impl q)\Wait p
\end{equation}

\emph{Proof}: The proof is by (4.7.1) Truth implication.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $(p\impl q)\Wait p$\\[\lgap]
\> $=$ \> \Hint{(3.59) Implication $p\impl q\equiv \neg p\lor q$} \\[\lgap]
\> \> $(\neg p \lor q)\Wait p$\\[\lgap]
\> $\foll$ \> \Hint{(\ref{E:rightWaitOrDist}) Right distributivity of $\Wait$ over $\lor$} \\[\lgap]
\> \> $\neg p \Wait p\lor q\Wait p$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:ruleWait}) Rule of $\Wait$} \\[\lgap]
\> \> $true\lor q\Wait p$\\[\lgap]
\> $=$ \> \Hint{(3.29) Zero of $\lor$} \\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:eventPImplPImplUntilp}
\Event p\impl(p\impl q)\Until p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $(p\impl q)\Until p$\\[\lgap]
\> $=$ \> \Hint{(3.59) Implication $p\impl q\equiv \neg p\lor q$} \\[\lgap]
\> \> $(\neg p\lor q)\Until p$\\[\lgap]
\> $\foll$ \> \Hint{(\ref{E:untilOrImp}) Right distributivity of $\Until$ over $\lor$} \\[\lgap]
\> \> $\neg p \Until p\lor q\Until p$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:ruleUntil}) Rule of $\Until$} \\[\lgap]
\> \> $\Event p\lor q\Until p$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilFromWait}) $\Until$ in terms of $\Wait$} \\[\lgap]
\> \> $\Event p\lor (q\Wait p\land \Event p)$\\[\lgap]
\> $=$ \> \Hint{(3.43b) Absorption $p\lor (p\land q)\equiv p$} \\[\lgap]
\> \> $\Event p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:conRuleWait}
\textbf{Conjunction rule of $\Wait$:}\quad p\Wait q\equiv (p\land \neg q)\Wait q
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:disRuleWait}) Disjunction rule of $\Wait$} \\[\lgap]
\> \> $(p\lor q)\Wait q$\\[\lgap]
\> $=$ \> \Hint{(3.39) Identity of $\land$, $p\land true \equiv p$} \\[\lgap]
\> \> $(p\lor q)\Wait q\land true$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:ruleWait}) Rule of $\Wait$} \\[\lgap]
\> \> $(p\lor q)\Wait q\land \neg q\Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:rightWaitAndDist}) Right distributivity of $\Wait$ over $\land$} \\[\lgap]
\> \> $((p\lor q)\land \neg q)\Wait q$\\[\lgap]
\> $=$ \> \Hint{(3.44a) Absorption, $p\land (\neg p\lor q) \equiv p\land q$ with $p,q := \neg q,p$} \\[\lgap]
\> \> $(p\land \neg q) \Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:conRuleUntil}
\textbf{Conjunction rule of $\Until$:}\quad p\Until q\equiv (p\land \neg q)\Until q
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $(p\land \neg q)\Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilFromWait}) $\Until$ in terms of $\Wait$} \\[\lgap]
\> \> $(p\land \neg q)\Wait q \land \Event q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:conRuleWait}) Conjunction rule of $\Wait$} \\[\lgap]
\> \> $p\Wait q \land \Event q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilFromWait}) $\Until$ in terms of $\Wait$} \\[\lgap]
\> \> $p \Until q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:notWait2}
\textbf{Distributivity of $\neg$ over $\Wait$:}\quad \neg(p\Wait q)\equiv (p\land \neg q)\Until(\neg p\land \neg q)
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\neg (p\Wait q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:notWait}) Distributivity of $\neg$ over $\Wait$} \\[\lgap]
\> \> $\neg q \Until (\neg p \land \neg q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:conRuleUntil}) Conjunction rule of $\Until$ with $p,q:=\neg q, \neg p\land\neg q$} \\[\lgap]
\> \> $(\neg q \land \neg(\neg p \land \neg q)) \Until (\neg p \land \neg q)$\\[\lgap]
\> $=$  \>  \Hint{(3.47a) De Morgan, $\neg(p\land q)\equivs \neg p\lor\neg q$}\\[\lgap]
\> \> $(\neg q \land (p \lor q)) \Until (\neg p \land \neg q)$\\[\lgap]
\> $=$ \> \Hint{(3.44a) Absorption, $p\land (\neg p\lor q)\equiv p\land q$ with $p,q:=\neg q,p$} \\[\lgap]
\> \> $(p \land \neg q) \Until (\neg p \land \neg q)$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:notUntil2}
\textbf{Distributivity of $\neg$ over $\Until$:}\quad \neg(p\Until q)\equiv (p\land \neg q)\Wait(\neg p\land \neg q)
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\neg (p\Until q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:notUntil}) Distributivity of $\neg$ over $\Until$} \\[\lgap]
\> \> $\neg q \Wait (\neg p \land \neg q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:conRuleWait}) Conjunction rule of $\Wait$ with $p,q:=\neg q, \neg p\land\neg q$} \\[\lgap]
\> \> $(\neg q \land \neg(\neg p \land \neg q)) \Wait (\neg p \land \neg q)$\\[\lgap]
\> $=$  \>  \Hint{(3.47a) De Morgan, $\neg(p\land q)\equivs \neg p\lor\neg q$}\\[\lgap]
\> \> $(\neg q \land (p \lor q)) \Wait (\neg p \land \neg q)$\\[\lgap]
\> $=$ \> \Hint{(3.44a) Absorption, $p\land (\neg p\lor q)\equiv p\land q$ with $p,q:=\neg q,p$} \\[\lgap]
\> \> $(p \land \neg q) \Wait (\neg p \land \neg q)$ \quad \myqed
\end{tabbing}

Like the \textit{until} operator, the \textit{wait} operator is idempotent.
$true$ is the right zero of both \textit{until} and \textit{wait}.
$false$ is the left identity of both \textit{until} and \textit{wait}.
\begin{equation}\label{E:idempWait}
\textbf{Idempotency of $\Wait$:}\quad p \Wait p \equiv p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait p$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p \lor p\Until p$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:idemUntil}) Idempotency of $\Until$} \\[\lgap]
\> \> $\Always p \lor p$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:absAlwaysIntoOr}) Absorption of $\lor$ into $\Always$}\\[\lgap]
\> \> $p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:rightZeroWait}
\textbf{Right zero of $\Wait$:}\quad p \Wait true \equiv true
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait true$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p \lor p\Until true$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:zeroUntil}) Right zero of $\Until$} \\[\lgap]
\> \> $\Always p \lor true$\\[\lgap]
\> $=$ \> \Hint{(3.29) Zero of $\lor$, $p\lor true\equiv true$}\\[\lgap]
\> \> $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:leftIdentWait}
\textbf{Left identity of $\Wait$:}\quad false \Wait q \equiv q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $false \Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always false \lor false\Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:alwaysFalse}) Falsehood of $\Always$} \\[\lgap]
\> \> $false \lor false\Until q$\\[\lgap]
\> $=$ \> \Hint{(3.30) Identity of $\lor$, $p\lor false\equiv p$} \\[\lgap]
\> \> $false\Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:leftIdUntil}) Left identity of $\Until$}\\[\lgap]
\> \> $q$ \quad \myqed
\end{tabbing}

Theorem (\ref{E:waitToOr}) for the \textit{wait} operator corresponds to theorem (\ref{E:untilImpOr}) for the \textit{until} operator.
It states that $p \Wait q$ is stronger than $p \lor q$.
Theorem (\ref{E:orToWait}) states that $\Always(p \lor q)$ is stronger than $p \Wait q$.

\begin{equation}\label{E:waitToOr}
p \Wait q \impl p \lor q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $q \lor (p \land \Next(p \Wait q))$\\[\lgap]
\> $\impl$ \> \Hint{(3.76d) $p\lor (q\land r) \impl p\lor q$} \\[\lgap]
\> \> $p \lor q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:orToWait}
\Always (p\lor q) \impl p \Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Always (p\lor q)$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:alwaysImpWait}) Perpetuity} \\[\lgap]
\> \> $(p\lor q)\Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:disRuleWait}) Disjunction rule of $\Wait$} \\[\lgap]
\> \> $p \Wait q$ \quad \myqed
\end{tabbing}

Insertion for the \textit{wait} operator corresponds to
(\ref{E:untilInsertion}) Insertion for the \textit{until} operator.
\begin{equation}\label{E:waitInsertion}
\textbf{Insertion:}\quad q \impl p \Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $q \lor (p \land \Next(p \Wait q))$\\[\lgap]
\> $\foll$ \> \Hint{(3.76a) Weakening, $p\impl p\lor q$} \\[\lgap]
\> \> $q$ \quad \myqed
\end{tabbing}

The next five absorption theorems correspond to the five absorption theorems for \textit{until},
(\ref{E:untilOrP}),
(\ref{E:untilOrQ}),
(\ref{E:untilAndQ}),
(\ref{E:untilAndOr}),
and
(\ref{E:untilOrAnd})
respectively.
\begin{equation}\label{E:waitOrP}
\textbf{Absorption:}\quad p\lor p\Wait q\equiv p\lor q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\lor p\Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p\lor p \Until q\lor \Always p$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:absAlwaysIntoOr}) Absorption of $\lor$ into $\Always$} \\[\lgap]
\> \> $p\lor p \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilOrP}) Absorption} \\[\lgap]
\> \> $p\lor q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitOrQ}
\textbf{Absorption:}\quad p\Wait q\lor q\equiv p\Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\Wait q\lor q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $q\lor (p\land \Next (p\Wait q)) \lor q$\\[\lgap]
\> $=$ \> \Hint{(3.26) Idempotency of $\lor$, $p \lor p \equiv p$} \\[\lgap]
\> \> $q\lor (p\land \Next (p\Wait q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $p\Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitAndQ}
\textbf{Absorption:}\quad p\Wait q\land q\equiv q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\Wait q\land q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $(q\lor (p\land \Next (p\Wait q))) \land q$\\[\lgap]
\> $=$ \> \Hint{(3.43a) Absorption $p \land (p \lor q) \equiv p$} \\[\lgap]
\> \> $q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitAndOr}
\textbf{Absorption:}\quad p\Wait q\land (p\lor q) \equiv p\Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\Wait q\land (p\lor q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $(q\lor (p\land \Next (p\Wait q))) \land (p\lor q)$\\[\lgap]
\> $=$ \> \Hint{(3.45) Distributivity of $\lor$ over $\land$, $p\lor (q\land r)\equiv (p\lor q)\land (p\lor r)$} \\[\lgap]
\> \> $q\lor (p\land \Next (p\Wait q) \land p)$\\[\lgap]
\> $=$ \> \Hint{(3.38) Idempotency of $\land$, $p \land p \equiv p$} \\[\lgap]
\> \> $q\lor (p\land \Next (p\Wait q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $p\Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitOrAnd}
\textbf{Absorption:}\quad p\Wait q\lor (p\land q) \equiv p\Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p\Wait q\lor (p\land q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $q\lor (p\land \Next (p\Wait q)) \lor (p\land q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.43b) Absorption $p \lor (p \land q) \equiv p$ with $p,q:=q,p$}\\[\lgap]
\> \> $q\lor (p\land \Next (p\Wait q))$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:expansionWait}) Expansion of $\Wait$} \\[\lgap]
\> \> $p\Wait q$ \quad \myqed
\end{tabbing}

The left and right absorption theorems for $\Wait$ correspond to, and are proved from, the left and right absorption theorems
for $\Until$, (\ref{E:untilIdem}) and (\ref{E:untilIdemR}).
\begin{equation}\label{E:waitAbsL}
\textbf{Left absorption of $\Wait$:}\quad p \Wait (p \Wait q) \equiv p \Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Wait (p \Wait q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$ twice} \\[\lgap]
  \> \>   $p \Until (p \Until q \lor \Always p) \lor \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilOrEquiv}) Left distributivity of $\Until$ over $\lor$}\\[\lgap]
  \> \>   $p \Until (p \Until q) \lor p\Until \Always p \lor \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:absUntilAlways}) Absorption of $\Until$ into $\Always$ and (3.26) Idempotency of $\lor$, $p\lor p \equiv p$}\\[\lgap]
  \> \>   $p \Until (p \Until q) \lor \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilIdem}) Left absorption of $\Until$}\\[\lgap]
  \> \>   $p \Until q \lor \Always p$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
  \> \>   $p \Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitAbsR}
\textbf{Right absorption of $\Wait$:}\quad (p \Wait q) \Wait q \equiv p \Wait q
\end{equation}

\emph{Proof}: The proof is by (4.7) Mutual implication.
The proof in the first direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $(p \Wait q)\Wait q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defWait}) Definition of $\Wait$}\\[\lgap]
  \> \>   $(p \Until q\lor \Always p)\Wait q$\\[\lgap]
  \> $\foll$  \>  \Hint{(\ref{E:rightWaitOrDist}) Right distributivity of $\Wait$ over $\lor$}\\[\lgap]
  \> \>   $(p \Until q)\Wait q \lor \Always p\Wait q$\\[\lgap]
  \> $\foll$  \>  \Hint{(\ref{E:untilImplWait}) and (4.2) Monotonicity of $\lor$}\\[\lgap]
  \> \>   $(p \Until q)\Until q \lor \Always p\Wait q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilIdemR}) Right absorption of $\Until$}\\[\lgap]
  \> \>   $p \Until q \lor \Always p\Wait q$\\[\lgap]
  \> $\foll$  \>  \Hint{(\ref{E:alwaysImpWait}) Perpetuity and (4.2) Monotonicity of $\lor$}\\[\lgap]
  \> \>   $p \Until q \lor \Always \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:IdemAlways}) Absorption of $\Always$}\\[\lgap]
  \> \>   $p \Until q \lor \Always p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:defWait}) Definition of $\Wait$}\\[\lgap]
  \> \>   $p \Wait q$
\end{tabbing}
The proof in the second direction follows.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $(p \Wait q) \Wait q$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:waitToOr})}\\[\lgap]
  \> \>   $p \Wait q \lor q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:waitOrQ}) Absorption}\\[\lgap]
  \> \>   $p \Wait q$ \quad \myqed
\end{tabbing}

\begin{figure}[t]
\centering
\renewcommand\arraystretch{1.2}
\begin{tabular}{ l l }
  \toprule
  (\ref{E:untilFalse}) Right zero of $\Until$:\; $p \Until false \equiv false$
  &
  (\ref{E:leftZeroWait}) Left zero of $\Wait$:\; $true \Wait q \equiv true$ \\
  \midrule
  (\ref{E:zeroUntil}) Right zero of $\Until$:\; $p \Until true \equiv true$
  &
  (\ref{E:rightZeroWait}) Right zero of $\Wait$:\; $p \Wait true \equiv true$ \\
  \midrule
  (\ref{E:leftIdUntil}) Left identity of $\Until$:\; $false \Until q \equiv q$
  &
  (\ref{E:leftIdentWait}) Left identity of $\Wait$:\; $false \Wait q \equiv q$ \\
  \midrule
  (\ref{E:defEvent}) $true \Until q \equiv \Event q$
  &
  (\ref{E:alwaysAsWait}) $p \Wait false\equiv \Always p$ \\
  \bottomrule
\end{tabular}
\renewcommand\arraystretch{1}
\caption{The eight possibilities of $true$ and $false$ on the left hand side and right hand side of $\Until$ and $\Wait$.
\label{true-false-wait-until}}
\end{figure}

The following theorem corresponds to the definition of the \textit{eventually} operator (\ref{E:defEvent}).
Figure \ref{true-false-wait-until} summarizes the eight possibilities of $true$ and $false$ on the left hand side and right hand side of $\Until$ and $\Wait$.
\begin{equation}\label{E:alwaysAsWait}
\Always p \equiv p \Wait false
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait false$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p\lor p \Until false$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilFalse}) Right zero of $\Until$} \\[\lgap]
\> \> $\Always p\lor false$\\[\lgap]
\> $=$ \> \Hint{(3.30) Identity of $\lor$, $p\lor false\equiv p$} \\[\lgap]
\> \> $\Always p$ \quad \myqed
\end{tabbing}

The following theorem for the \textit{wait} operator corresponds to (\ref{E:axiomUntilImpl}) $\Until$ implication.
\begin{equation}\label{E:waitEntailment}
\textbf{$\Wait$ implication:}\quad p \Wait q \impl \Always p\lor \Event q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p\lor p \Until q$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:eventuality}) Eventuality and (4.2) Monotonicity of $\lor$} \\[\lgap]
\> \> $\Always p\lor \Event q$ \quad \myqed
\end{tabbing}

Each of the following four absorption theorems combine an \textit{until} operation with a \textit{wait} operation.
\begin{equation}\label{E:leftWaitAbsUtil}
\textbf{Absorption:}\quad p \Wait (p \Until q) \equiv p \Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait (p \Until q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p\lor p \Until (p \Until q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilIdem}) Left absorption of $\Until$} \\[\lgap]
\> \> $\Always p\lor p \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p \Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:rightWaitAbsUtil}
\textbf{Absorption:}\quad (p \Until q) \Wait q \equiv p \Until q
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $(p \Until q) \Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always (p \Until q)\lor (p \Until q) \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilIdemR}) Right absorption of $\Until$} \\[\lgap]
\> \> $\Always (p \Until q)\lor p \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:absAlwaysIntoOr}) Absorption of $\Always$ into $\lor$ with $p := p\Until q$} \\[\lgap]
\> \> $p \Until q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:leftUntilAbsWait}
\textbf{Absorption:}\quad p \Until (p \Wait q) \equiv p \Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Until (p \Wait q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p \Until (\Always p\lor p \Until q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilOrEquiv}) Left Distributivity of $\Until$ over $\lor$} \\[\lgap]
\> \> $p \Until \Always p\lor p \Until (p \Until q)$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilIdem}) Left absorption of $\Until$} \\[\lgap]
\> \> $p \Until \Always p\lor p \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:absUntilAlways}) Absorption} \\[\lgap]
\> \> $\Always p\lor p \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p \Wait q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:rightUntilAbsWait}
\textbf{Absorption:}\quad (p \Wait q) \Until q \equiv p \Until q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $(p \Wait q) \Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilFromWait}) $\Until$ in terms of $\Wait$} \\[\lgap]
\> \> $(p \Wait q) \Wait q \land \Event q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:waitAbsR}) Right absorption of $\Wait$} \\[\lgap]
\> \> $p \Wait q \land \Event q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:untilFromWait}) $\Until$ in terms of $\Wait$} \\[\lgap]
\> \> $p \Until q$ \quad \myqed
\end{tabbing}

The following theorem corresponds to (\ref{E:absUntilAlways}) Absorption of $\Until$ into $\Always$.
\begin{equation}\label{E:absorpEventWait}
\textbf{Absorption of $\Wait$ into $\Event$:}\quad \Event q \Wait q \equiv \Event q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Event q \Wait q$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
\> \> $(true\Until q) \Wait q$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:rightWaitAbsUtil}) Absorption}\\[\lgap]
\> \> $true\Until q$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:defEvent}) Definition of $\Event$}\\[\lgap]
\> \> $\Event q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:absWaitAlways}
\textbf{Absorption of $\Wait$ into $\Always$:}\quad \Always p\land p\Wait q\equiv \Always p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Always p\land p\Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p\land (\Always p\lor p\Until q)$\\[\lgap]
\> $=$ \> \Hint{(3.43a) Absorption $p\land (p\lor q) \equiv p$} \\[\lgap]
\> \> $\Always p$ \quad \myqed
\end{tabbing}
The following theorem corresponds to (\ref{E:absEventIntoUntil}) Absorption of $\Event$ into $\Until$. 
\begin{equation}\label{E:absAlwaysWait}
\textbf{Absorption of $\Always$ into $\Wait$:}\quad \Always p\lor p\Wait q\equiv p\Wait q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\Always p\lor p\Wait q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $\Always p\lor \Always p\lor p\Until q$\\[\lgap]
\> $=$ \> \Hint{(3.26) Idempotency of $\lor$, $p \lor p \equiv p$} \\[\lgap]
\> \> $\Always p\lor p\Until q$\\[\lgap]
\> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
\> \> $p\Wait q$ \quad \myqed
\end{tabbing}

The next two pair of theorems correspond.
The \textit{wait} versions are in the temporal logic literature.
The \textit{until} versions are apparently unique to this system.
\begin{equation}\label{E:waitEntailAlways}
p \Wait q \land \Always\neg q \impl \Always p
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait q \land \Always\neg q$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:waitEntailment}) $\Wait$ implication and (4.3) Monotonicity of $\land$} \\[\lgap]
\> \> $(\Always p \lor \Event q) \land \Always\neg q$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
\> \> $(\Always p \lor \Event q) \land \neg \Event q$\\[\lgap]
\> $=$ \> \Hint{(3.44a) Absorption, $p\land (\neg p\lor q)\equiv p\land q$} \\[\lgap]
\> \> $\Always p \land \neg \Event q$\\[\lgap]
\> $\impl$ \> \Hint{(3.76b) Strengthening, $p\land q \impl p$} \\[\lgap]
\> \> $\Always p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:untilEntailAlways}
\Always p\impl p \Until q \lor \Always\neg q 
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Until q \lor \Always\neg q$\\[\lgap]
\> $\foll$ \> \Hint{(\ref{E:axiomUntilImpl}) $\Until$ implication and (4.2) Monotonicity of $\lor$} \\[\lgap]
\> \> $(\Always p \land \Event q) \lor \Always\neg q$\\[\lgap]
\> $=$  \>  \Hint{(\ref{E:dualEvent}) Dual of $\Event$}\\[\lgap]
\> \> $(\Always p \land \Event q) \lor \neg \Event q$\\[\lgap]
\> $=$  \>  \Hint{(3.44b) Absorption, $p \lor (\neg p \land q) \equiv p \lor q$}\\[\lgap]
\> \> $\Always p \lor \neg \Event q$\\[\lgap]
\> $\foll$ \> \Hint{(3.76a) Weakening, $p\impl p\lor q$} \\[\lgap]
\> \> $\Always p$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitEntailEvent}
\neg\Always p\land p \Wait q \impl \Event q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\neg\Always p\land p \Wait q$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:waitEntailment}) $\Wait$ implication and (4.3) Monotonicity of $\land$} \\[\lgap]
\> \> $\neg\Always p\land (\Always p \lor \Event q)$\\[\lgap]
\> $=$ \> \Hint{(3.44a) Absorption, $p\land (\neg p\lor q)\equiv p\land q$} \\[\lgap]
\> \> $\neg\Always p\land \Event q$\\[\lgap]
\> $\impl$ \> \Hint{(3.76b) Strengthening, $p\land q \impl p$} \\[\lgap]
\> \> $\Event q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:untilEntailEvent}
\Event q\impl \neg\Always p\lor p \Until q
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $\neg\Always p\lor p \Until q$\\[\lgap]
\> $\foll$ \> \Hint{(\ref{E:axiomUntilImpl}) $\Until$ implication and (4.2) Monotonicity of $\lor$} \\[\lgap]
\> \> $\neg\Always p\lor (\Always p\land \Event q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.44b) Absorption, $p \lor (\neg p \land q) \equiv p \lor q$}\\[\lgap]
\> \> $\neg\Always p\lor \Event q$\\[\lgap]
\> $\foll$ \> \Hint{(3.76a) Weakening, $p\impl p\lor q$} \\[\lgap]
\> \> $\Event q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:rightMonoUntil}
\textbf{Right monotonicity of $\Until$:}\quad \Always (p \impl q) \impl (r \Until p \impl r \Until q)
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \impl q) \impl (r \Until p \impl r \Until q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.65) Shunting, $p\land q \impl r \equivs p \impl (q \impl r)$}\\[\lgap]
  \> \>   $\Always (p \impl q) \land r \Until p \impl r \Until q$\\[\lgap]
  \> $=$  \>  \Hint{Lemma: $\Always (p \impl q) \land r \Until p \impl r \Until q$}\\[\lgap]
  \> \>   $true$
\end{tabbing}

\emph{Proof of Lemma}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \impl q) \land r \Until p$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:andUntilDist}) Distributivity of $\land$ over $\Until$}\\[\lgap]
  \> \>   $((p \impl q) \land r) \Until ((p \impl q) \land p)$\\[\lgap]
  \> $=$  \>  \Hint{(3.66) $p\land p \impl q \equivs  p \land q$}\\[\lgap]
  \> \>   $((p \impl q) \land r) \Until (p \land q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:untilAndEquiv}) Right Distributivity of $\Until$ over $\land$}\\[\lgap]
  \> \>   $((p \impl q) \Until (p \land q) \land r \Until (p \land q)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:untilAndImp}) Left Distributivity of $\Until$ over $\land$ and (4.3) Monotonicity of $\land$}\\[\lgap]
  \> \>   $((p \impl q) \Until (p \land q) \land r \Until p \land r \Until q$\\[\lgap]
  \> $\impl$ \> \Hint{(3.76b) Strengthening, $p\land q \impl p$} \\[\lgap]
  \> \>   $r \Until q$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:leftMonoWait}
\textbf{Left monotonicity of $\Wait$:}\quad \Always (p \impl q) \impl (p \Wait r \impl q \Wait r)
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \impl q) \impl (p \Wait r \impl q \Wait r)$\\[\lgap]
  \> $=$  \>  \Hint{(3.65) Shunting, $p\land q \impl r \equivs p \impl (q \impl r)$}\\[\lgap]
  \> \>   $\Always (p \impl q) \land p \Wait r \impl q \Wait r$\\[\lgap]
  \> $=$  \>  \Hint{Lemma: $\Always (p \impl q) \land p \Wait r \impl q \Wait r$}\\[\lgap]
  \> \>   $true$
\end{tabbing}

\emph{Proof of Lemma}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p => q) \land p \Wait r$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:andWaitDist}) Distributivity of $\land$ over $\Wait$}\\[\lgap]
  \> \>   $((p \impl q) \land p) \Wait ((p \impl q) \land r)$\\[\lgap]
  \> $=$  \>  \Hint{(3.66) $p\land p \impl q \equivs  p \land q$}\\[\lgap]
  \> \>   $((p \land q) \Wait ((p \impl q) \land r)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:leftWaitAndDist}) Left Distributivity of $\Wait$ over $\land$}\\[\lgap]
  \> \>   $((p \land q) \Wait (p \impl q) \land (p \land q) \Wait r$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:rightWaitAndDist}) Right Distributivity of $\Wait$ over $\land$}\\[\lgap]
  \> \>   $((p \land q) \Wait (p \impl q) \land p \Wait r \land q \Wait r$\\[\lgap]
  \> $\impl$ \> \Hint{(3.76b) Strengthening, $p\land q \impl p$} \\[\lgap]
  \> \>   $q \Wait r$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:leftMonoUntil}
\textbf{Left monotonicity of $\Until$:}\quad \Always (p \impl q) \impl (p \Until r \impl q \Until r)
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p \Until r \impl q \Until r$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:untilFromWait}) $\Until$ in terms of $\Wait$} \\[\lgap]
  \> \>   $p \Wait r \land \Event r\impl q \Wait r \land \Event r$\\[\lgap]
  \> $\foll$  \>  \Hint{(4.3) Monotonicity of $\land$, $(p\impl q)\impl (p\land r \impl q\land r)$}\\[\lgap]
  \> \>   $p \Wait r \impl q \Wait r$\\[\lgap]
  \> $\foll$  \>  \Hint{(\ref{E:leftMonoWait}) Left monotonicity of $\Wait$}\\[\lgap]
  \> \>   $\Always (p \impl q)$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:rightMonoWait}
\textbf{Right monotonicity of $\Wait$:}\quad \Always (p \impl q) \impl (r \Wait p \impl r \Wait q)
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $r \Wait p \impl r \Wait q$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:defWait}) Definition of $\Wait$} \\[\lgap]
  \> \>   $\Always r \lor r \Until p \impl \Always r \lor r \Until q$\\[\lgap]
  \> $\foll$  \>  \Hint{(4.2) Monotonicity of $\lor$, $(p\impl q)\impl (p\lor r \impl q\lor r)$}\\[\lgap]
  \> \>   $r \Until p \impl r \Until q$\\[\lgap]
  \> $\foll$  \>  \Hint{(\ref{E:rightMonoUntil}) Right monotonicity of $\Until$}\\[\lgap]
  \> \>   $\Always (p \impl q)$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitImpAbsR}
\textbf{Absorption:}\quad (p \Wait q) \Wait r \impl (p \lor q) \Wait r
\end{equation}

\emph{Proof}: The proof is by (4.7.1) Truth implication.
By (\ref{E:metatheorem}) Metatheorem and (\ref{E:waitToOr}), $\Always (p\Wait q\impl p\lor q)$ is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $true$\\[\lgap]
  \> $=$ \> \Hint{$\Always (p\Wait q\impl p\lor q)$ is a theorem} \\[\lgap]
  \> \>   $\Always (p\Wait q\impl p\lor q)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:rightMonoWait}) Right monotonicity of $\Wait$ with $p,q,r := p\land \neg q, p, \neg q$}\\[\lgap]
  \> \>   $(p \Wait q) \Wait r \impl (p \lor q) \Wait r$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitImpAbsL}
\textbf{Absorption:}\quad p \Wait (q \Wait r) \impl (p \lor q) \Wait r
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
\> \> $p \Wait (q \Wait r)$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:waitAssocImp}) Weak associativity of $\Wait$}\\[\lgap]
\> \> $(p \Wait q) \Wait r$\\[\lgap]
\> $\impl$ \> \Hint{(\ref{E:waitImpAbsR}) Absorption} \\[\lgap]
\> \> $(p \lor q) \Wait r$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitOrderingThree}
\textbf{Ordering:}\quad p \Wait (q \land r) \impl (p \Wait q) \Wait r
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $p\Wait (q\land r)$\\[\lgap]
  \> $\impl$  \>  \Hint{Lemma a: $p\Wait (r\land q)\impl p\Wait r$}\\[\lgap]
  \> \>   $p \Wait r$\\[\lgap]
  \> $\impl$  \>  \Hint{Lemma b: $p\Wait r\impl p\Wait (q\Wait r)$}\\[\lgap]
  \> \>   $p \Wait (q \Wait r)$\\[\lgap]
  \> $\impl$ \> \Hint{(\ref{E:waitAssocImp}) Weak associativity of $\Wait$}\\[\lgap]
  \> \>   $(p \Wait q) \Wait r$
\end{tabbing}
\emph{Proof of Lemma a}: The proof is by (4.7.1) Truth implication.
(3.76b) Strengthening the antecedent $p\land q\impl p$ with $p := r$ is $r\land q\impl r$.
Therefore, by (\ref{E:metatheorem}) Metatheorem, $\Always (r\land q\impl r)$ is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $true$\\[\lgap]
  \> $=$  \>  \Hint{$\Always (r\land q\impl r)$ is a theorem}\\[\lgap]
  \> \>   $\Always (r\land q\impl r)$\\[\lgap]
  \> $\impl$ \> \Hint{(\ref{E:rightMonoWait}) Right monotonicity of $\Wait$ with $p,q,r:=r\land q,r,p$} \\[\lgap]
  \> \>   $p\Wait(r\land q)\impl p\Wait r$
\end{tabbing}
\emph{Proof of Lemma b}: The proof is by (4.7.1) Truth implication.
(\ref{E:waitInsertion}) Insertion with $p,q := q,r$ is $r\impl q\Wait r$.
Therefore, by (\ref{E:metatheorem}) Metatheorem, $\Always (r\impl q\Wait r)$ is a theorem.
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $true$\\[\lgap]
  \> $=$  \>  \Hint{$\Always (r\impl q\Wait r)$ is a theorem}\\[\lgap]
  \> \>   $\Always (r\impl q\Wait r)$\\[\lgap]
  \> $\impl$ \> \Hint{(\ref{E:rightMonoWait}) Right monotonicity of $\Wait$ with $p,q,r:=r,q\Wait r,p$} \\[\lgap]
  \> \>   $p\Wait r\impl p\Wait (q\Wait r)$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitOrdering}
\textbf{Ordering:}\quad \neg p \Wait q \lor \neg q \Wait p
\end{equation}

\emph{Proof}: (Scott Staley)
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\neg p \Wait q \lor \neg q \Wait p$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:conRuleWait}) Conjunction rule of $\Wait$ twice}\\[\lgap]
  \> \>   $(\neg p\land \neg q) \Wait q \lor (\neg q \land \neg p)\Wait p$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:waitOrDist}) Left distributivity of $\Wait$ over $\lor$}\\[\lgap]
  \> \>   $(\neg p\land \neg q) \Wait (p\lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(3.47a) De Morgan, $\neg(p\land q)\equivs \neg p\lor\neg q$}\\[\lgap]
  \> \>   $\neg (p\lor q)\Wait (p\lor q)$\\[\lgap]
  \> $=$  \>  \Hint{(\ref{E:ruleWait}) Rule of $\Wait$ with $q := p\lor q$}\\[\lgap]
  \> \>   $true$ \quad \myqed
\end{tabbing}
\begin{equation}\label{E:waitOrderingTwo}
\textbf{Ordering:}\quad \Always (p \Wait q \land \neg q \Wait r) \impl p \Wait r
\end{equation}

\emph{Proof}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $\Always (p \Wait q \land \neg q \Wait r)$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
  \> \>   $\Always (p \Wait q) \land \Always(\neg q \Wait r)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:metaAlways}) Metatheorem $\Always$ with (\ref{E:waitToOr}) and (4.3) Monotonicity of $\land$, twice}\\[\lgap]
  \> \>   $\Always (p \lor q) \land \Always(\neg q \lor r)$\\[\lgap]
  \> $=$ \> \Hint{(\ref{E:distAlwaysAnd}) Distributivity of $\Always$ over $\land$}\\[\lgap]
  \> \>   $\Always ((p \lor q) \land (\neg q \lor r))$\\[\lgap]
  \> $\impl$  \>  \Hint{Lemma: $\Always ((p \lor q) \land (\neg q \lor r))\impl \Always(p\lor r)$}\\[\lgap]
  \> \>   $\Always (p \lor r)$\\[\lgap]
  \> $\impl$  \>  \Hint{(\ref{E:orToWait})}\\[\lgap]
  \> \>   $p\Wait r$
\end{tabbing}

\emph{Proof of Lemma}:
\begin{tabbing}
\hspace{\mymathindent} \= $= \;$ \= \myqedtab \= \kill
  \> \>   $(p\lor q)\land (\neg q\lor r)$\\[\lgap]
  \> $=$  \>  \Hint{(3.76b) Distributivity of $\land$ over $\lor$, $p\land(q\lor r) \equiv (p\land q)\lor (p\land r)$}\\[\lgap]
  \> \>   $(p\land (\neg q\lor r))\lor (q\land (\neg q\lor r))$\\[\lgap]
  \> $\impl$  \>  \Hint{(3.76b) Strengthening, $p\land q \impl p$ and (4.2) Monotonicity of $\lor$}\\[\lgap]
  \> \>   $p\lor (q\land (\neg q\lor r))$\\[\lgap]
  \> $=$  \>  \Hint{(3.44a) Absorption, $p\land (\neg p\lor q)\equiv p\land q$}\\[\lgap]
  \> \>   $p\lor (q\land r)$\\[\lgap]
  \> $\impl$  \>  \Hint{(3.76b) Strengthening, $p\land q \impl p$ and (4.2) Monotonicity of $\lor$}\\[\lgap]
  \> \>   $p\lor r$
\end{tabbing}
The above proof shows that $(p\lor q)\land (\neg q\lor r) \impl p\lor r$ is a theorem.
Therefore, by (\ref{E:metaAlways}) Metatheorem $\Always$, $\Always ((p\lor q)\land (\neg q\lor r)) \impl \Always (p\lor r)$ is a theorem. \quad \myqed

\section{Comparison with previous work}\label{comparison-previous-work}

As a check on comprehensiveness, we inventoried all the linear temporal logic theorems in Kröger and Merz\cite{Kroger}, Manna and Pnueli \cite{Manna}, Schneider \cite{Schn}, Emerson \cite{Emer}, and Ben-Ari \cite{Ben2}.
This section compares the axiomatization systems of those sources with this work.

\subsection{Kröger and Merz}

\subsection{Manna and Pnueli}

\subsection{Schneider}

\subsection{Emerson}

\subsection{Ben-Ari}

\subsection{New theorems}

This paper presents 44 linear temporal logic theorems not included in any of the above cited references.
Two are the axioms
(\ref{E:absUntilAlways}) Absorption and
(\ref{E:axiomUntilImpl}) $\Until$ implication.

The remaining 41 are the theorems
(\ref{E:nextTruth}) Truth of $\Next$,
(\ref{E:nextFalse}) Falsehood of $\Next$,
(\ref{E:untilFalse}),
(\ref{E:zeroUntil}),
(\ref{E:leftIdUntil}),
(\ref{E:untilOrP}) Absorption,
(\ref{E:untilOrQ}) Absorption,
(\ref{E:untilAndQ}) Absorption,
(\ref{E:untilAndOr}) Absorption,
(\ref{E:untilOrAnd}) Absorption,
(\ref{E:eventTrue}) Truth of $\Event$,
(\ref{E:eventFalse}) Falsehood of $\Event$,
(\ref{E:absOrIntoEvent}) Absorption of $\lor$ into $\Event$,
(\ref{E:absEventIntoAnd}) Absorption of $\land$ into $\Event$,
(\ref{E:alwaysTrue}) Truth of $\Always$,
(\ref{E:alwaysFalse}) Falsehood of $\Always$,
(\ref{E:absAndIntoAlways}) Absorption of $\land$ into $\Always$,
(\ref{E:absAlwaysIntoOr}) Absorption of $\lor$ into $\Always$,
(\ref{E:impNext}),
(\ref{E:metatheorem}) Metatheorem,
(\ref{E:untilFromWait}) $\Until$ in terms of $\Wait$,
(\ref{E:leftZeroWait}) Left zero of $\Wait$,
(\ref{E:idempWait}) Idempotency of $\Wait$,
(\ref{E:rightZeroWait}) Right zero of $\Wait$,
(\ref{E:leftIdentWait}) Left identity of $\Wait$,
(\ref{E:untilImplWait}),
(\ref{E:waitOrP}) Absorption,
(\ref{E:waitOrQ}) Absorption,
(\ref{E:waitAndQ}) Absorption,
(\ref{E:waitAndOr}) Absorption,
(\ref{E:waitOrAnd}) Absorption,
(\ref{E:absEventIntoUntil}) Absorption of $\Event$ into $\Until$,
(\ref{E:absAlwaysWait}) Absorption of $\Always$ into $\Wait$,
(\ref{E:untilEntailAlways}),
(\ref{E:untilEntailEvent}),
(\ref{E:rightUntilAbsWait}) Absorption,
(\ref{E:absorpEventWait}) Absorption,
(\ref{E:leftMonoUntil}) Left monotonicity of $\Until$,
(\ref{E:rightMonoUntil}) Right monotonicity of $\Until$,
(\ref{E:notUntil}) Distributivity of $\neg$ over $\Until$,
(\ref{E:notWait}) Distributivity of $\neg$ over $\Wait$.

\section{Conclusion}

Dijkstra and Scholten \cite{DandS}, and Feijen \cite{Feij} originally developed $\mathcal{E}$ as a logic system to prove
program correctness based on an equational style.
Gries and Schneider extend that system to a theory of sets, a theory of sequences,
relations and functions, a theory of integers, recurrence relations, modern algebra, and a theory of graphs.
Similarly, this system extends $\mathcal{E}$ to a theory of linear temporal logic.
It takes unary operator \textit{next} $\Next$ and binary operator \textit{until} $\Until$ as primitives and defines
\textit{eventually} $\Event$, \textit{always} $\Always$, and \textit{wait} $\Wait$ in terms of them.

This paper presents an axiomatic deductive system of linear temporal logic whose theorems are proved with the equational
logic $\mathcal{E}$ of Gries and Schneider \cite{LADM}.
The equational deductive system $\mathcal{E}$ has several advantages over other logic systems.
The primary advantage is that the equational system has only one proof rule, Leibniz.
Consequently, proofs of theorems are easier to understand and more intuitive to those schooled in that system.
Neither of the authors, the first of whom was an undergraduate student when most of this work was done,
has formal training in linear temporal systems.

In our judgement, the progress we were able to make in exploring the structure of linear temporal systems
is directly attributable to our training in the equational deductive system $\mathcal{E}$.
We believe the advantages of $\mathcal{E}$ over other logic systems is so substantial that it should be the
tool of choice for computer science theory.
We hope that this extension of $\mathcal{E}$ to linear temporal logic will not only be of use in the
temporal logic community, but will serve as an example to promote $\mathcal{E}$ in the broader computer science community.

\bibliographystyle{plain}
\bibliography{Vega-Paper}
\end{document}
